Proofgold Address

Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem e70ba..^exandE_iii : ∀ x0 x1 : (ι → ι → ι) → ο . (∃ x2 : ι → ι → ι . and (x0 x2) (x1 x2)) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Theorem b35ea..^exandE_iiii : ∀ x0 x1 : (ι → ι → ι → ι) → ο . (∃ x2 : ι → ι → ι → ι . and (x0 x2) (x1 x2)) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Theorem 9132c..^exandE_iio : ∀ x0 x1 : (ι → ι → ο) → ο . (∃ x2 : ι → ι → ο . and (x0 x2) (x1 x2)) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Theorem 0f4a2..^exandE_iiio : ∀ x0 x1 : (ι → ι → ι → ο) → ο . (∃ x2 : ι → ι → ι → ο . and (x0 x2) (x1 x2)) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Definition Descr_ii^Descr_ii := λ x0 : (ι → ι) → ο . λ x1 . Eps_i (λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x1 = x2)
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)
Theorem Descr_ii_prop^{Descr_ii_prop} : ∀ x0 : (ι → ι) → ο . (∃ x1 : ι → ι . x0 x1) ⟶ (∀ x1 x2 : ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_ii x0)
Definition Descr_iii^Descr_iii := λ x0 : (ι → ι → ι) → ο . λ x1 x2 . Eps_i (λ x3 . ∀ x4 : ι → ι → ι . x0 x4 ⟶ x4 x1 x2 = x3)
Theorem Descr_iii_prop^{Descr_iii_prop} : ∀ x0 : (ι → ι → ι) → ο . (∃ x1 : ι → ι → ι . x0 x1) ⟶ (∀ x1 x2 : ι → ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iii x0)
Definition Descr_iio^Descr_iio := λ x0 : (ι → ι → ο) → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . x0 x3 ⟶ x3 x1 x2
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem Descr_iio_prop^{Descr_iio_prop} : ∀ x0 : (ι → ι → ο) → ο . (∃ x1 : ι → ι → ο . x0 x1) ⟶ (∀ x1 x2 : ι → ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iio x0)
Definition Descr_Vo1^Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo1_prop^{Descr_Vo1_prop} : ∀ x0 : (ι → ο) → ο . (∃ x1 : ι → ο . x0 x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0)
Definition Descr_Vo2^Descr_Vo2 := λ x0 : ((ι → ο) → ο) → ο . λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo2_prop^{Descr_Vo2_prop} : ∀ x0 : ((ι → ο) → ο) → ο . (∃ x1 : (ι → ο) → ο . x0 x1) ⟶ (∀ x1 x2 : (ι → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo2 x0)
Definition Descr_Vo3^Descr_Vo3 := λ x0 : (((ι → ο) → ο) → ο) → ο . λ x1 : (ι → ο) → ο . ∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo3_prop^{Descr_Vo3_prop} : ∀ x0 : (((ι → ο) → ο) → ο) → ο . (∃ x1 : ((ι → ο) → ο) → ο . x0 x1) ⟶ (∀ x1 x2 : ((ι → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo3 x0)
Definition Descr_Vo4^Descr_Vo4 := λ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . λ x1 : ((ι → ο) → ο) → ο . ∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo4_prop^{Descr_Vo4_prop} : ∀ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . (∃ x1 : (((ι → ο) → ο) → ο) → ο . x0 x1) ⟶ (∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo4 x0)
Definition 711f6..^If_ii := λ x0 : ο . λ x1 x2 : ι → ι . λ x3 . If_i x0 (x1 x3) (x2 x3)
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 7c9c7..^If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ 711f6.. x0 x1 x2 = x1
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem bc627..^If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ 711f6.. x0 x1 x2 = x2
Definition 0c026..^If_iii := λ x0 : ο . λ x1 x2 : ι → ι → ι . λ x3 x4 . If_i x0 (x1 x3 x4) (x2 x3 x4)
Theorem ce5db..^If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ 0c026.. x0 x1 x2 = x1
Theorem 1202f..^If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ 0c026.. x0 x1 x2 = x2
Definition 5011a..^If_Vo1 := λ x0 : ο . λ x1 x2 : ι → ο . λ x3 . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 36071..^If_Vo1_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . x0 ⟶ 5011a.. x0 x1 x2 = x1
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem 29836..^If_Vo1_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . not x0 ⟶ 5011a.. x0 x1 x2 = x2
Definition a113b..^If_iio := λ x0 : ο . λ x1 x2 : ι → ι → ο . λ x3 x4 . and (x0 ⟶ x1 x3 x4) (not x0 ⟶ x2 x3 x4)
Theorem 96e82..^If_iio_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . x0 ⟶ a113b.. x0 x1 x2 = x1
Theorem b6c73..^If_iio_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . not x0 ⟶ a113b.. x0 x1 x2 = x2
Definition 06f01..^If_Vo2 := λ x0 : ο . λ x1 x2 : (ι → ο) → ο . λ x3 : ι → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Theorem 083fe..^If_Vo2_1 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . x0 ⟶ 06f01.. x0 x1 x2 = x1
Theorem d4610..^If_Vo2_0 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . not x0 ⟶ 06f01.. x0 x1 x2 = x2
Definition 3dad2..^If_Vo3 := λ x0 : ο . λ x1 x2 : ((ι → ο) → ο) → ο . λ x3 : (ι → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Theorem 2a734..^If_Vo3_1 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . x0 ⟶ 3dad2.. x0 x1 x2 = x1
Theorem f6f11..^If_Vo3_0 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . not x0 ⟶ 3dad2.. x0 x1 x2 = x2
Definition eb5c9..^If_Vo4 := λ x0 : ο . λ x1 x2 : (((ι → ο) → ο) → ο) → ο . λ x3 : ((ι → ο) → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Theorem eadde..^If_Vo4_1 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 ⟶ eb5c9.. x0 x1 x2 = x1
Theorem 4223b..^If_Vo4_0 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . not x0 ⟶ eb5c9.. x0 x1 x2 = x2
Definition 61278.. := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . λ x2 : ι → ι . ∀ x3 : ι → (ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition 6445c..^In_rec_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . Descr_ii (61278.. x0 x1)
Theorem a4d18.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . In x3 x1 ⟶ 61278.. x0 x3 (x2 x3)) ⟶ 61278.. x0 x1 (x0 x1 x2)
Theorem 7cec9.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . 61278.. x0 x1 x2 ⟶ ∃ x3 : ι → ι → ι . and (∀ x5 . In x5 x1 ⟶ 61278.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Known 61ad0..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 2c9e0.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι . 61278.. x0 x1 x2 ⟶ 61278.. x0 x1 x3 ⟶ x2 = x3
Theorem 3124e.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 61278.. x0 x1 (6445c.. x0 x1)
Theorem 58891.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 61278.. x0 x1 (x0 x1 (6445c.. x0))
Theorem 3b5bd..^In_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6445c.. x0 x1 = x0 x1 (6445c.. x0)
Definition ca584.. := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . λ x2 : ι → ι → ι . ∀ x3 : ι → (ι → ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ι . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition 28408..^In_rec_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . Descr_iii (ca584.. x0 x1)
Theorem 94633.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x1 ⟶ ca584.. x0 x3 (x2 x3)) ⟶ ca584.. x0 x1 (x0 x1 x2)
Theorem f2e34.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ca584.. x0 x1 x2 ⟶ ∃ x3 : ι → ι → ι → ι . and (∀ x5 . In x5 x1 ⟶ ca584.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Theorem 53b27.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ι . ca584.. x0 x1 x2 ⟶ ca584.. x0 x1 x3 ⟶ x2 = x3
Theorem c7b81.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ca584.. x0 x1 (28408.. x0 x1)
Theorem 15004.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ca584.. x0 x1 (x0 x1 (28408.. x0))
Theorem fba8c..^{In_rec_iii_eq} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 28408.. x0 x1 = x0 x1 (28408.. x0)
Definition 6f52e.. := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . λ x2 : ι → ι → ο . ∀ x3 : ι → (ι → ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition 03431..^In_rec_iio := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . Descr_iio (6f52e.. x0 x1)
Theorem 23f38.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι → ο . (∀ x3 . In x3 x1 ⟶ 6f52e.. x0 x3 (x2 x3)) ⟶ 6f52e.. x0 x1 (x0 x1 x2)
Theorem 75c04.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . 6f52e.. x0 x1 x2 ⟶ ∃ x3 : ι → ι → ι → ο . and (∀ x5 . In x5 x1 ⟶ 6f52e.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Theorem 09ec8.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ο . 6f52e.. x0 x1 x2 ⟶ 6f52e.. x0 x1 x3 ⟶ x2 = x3
Theorem e071f.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6f52e.. x0 x1 (03431.. x0 x1)
Theorem dc49b.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6f52e.. x0 x1 (x0 x1 (03431.. x0))
Theorem ee928..^{In_rec_iio_eq} : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 03431.. x0 x1 = x0 x1 (03431.. x0)
Definition 6869c.. := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ι → (ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition f9c5e..^In_rec_Vo1 := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . Descr_Vo1 (6869c.. x0 x1)
Theorem 98d06.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . In x3 x1 ⟶ 6869c.. x0 x3 (x2 x3)) ⟶ 6869c.. x0 x1 (x0 x1 x2)
Theorem fc0f8.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ο . 6869c.. x0 x1 x2 ⟶ ∃ x3 : ι → ι → ο . and (∀ x5 . In x5 x1 ⟶ 6869c.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Theorem 8511d.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ο . 6869c.. x0 x1 x2 ⟶ 6869c.. x0 x1 x3 ⟶ x2 = x3
Theorem a9e6e.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6869c.. x0 x1 (f9c5e.. x0 x1)
Theorem d502e.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6869c.. x0 x1 (x0 x1 (f9c5e.. x0))
Theorem c87be..^{In_rec_Vo1_eq} : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . f9c5e.. x0 x1 = x0 x1 (f9c5e.. x0)
Definition 59843.. := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . λ x2 : (ι → ο) → ο . ∀ x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (ι → ο) → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition c2908..^In_rec_Vo2 := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . Descr_Vo2 (59843.. x0 x1)
Theorem 9be4c.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → (ι → ο) → ο . (∀ x3 . In x3 x1 ⟶ 59843.. x0 x3 (x2 x3)) ⟶ 59843.. x0 x1 (x0 x1 x2)
Theorem 1e053.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . 59843.. x0 x1 x2 ⟶ ∃ x3 : ι → (ι → ο) → ο . and (∀ x5 . In x5 x1 ⟶ 59843.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Theorem edb50.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (ι → ο) → ο . 59843.. x0 x1 x2 ⟶ 59843.. x0 x1 x3 ⟶ x2 = x3
Theorem 56b05.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 59843.. x0 x1 (c2908.. x0 x1)
Theorem 71f3a.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 59843.. x0 x1 (x0 x1 (c2908.. x0))
Theorem 61a08..^{In_rec_Vo2_eq} : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . c2908.. x0 x1 = x0 x1 (c2908.. x0)
Definition 31b02.. := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . λ x2 : ((ι → ο) → ο) → ο . ∀ x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → ((ι → ο) → ο) → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition 2bbaf..^In_rec_Vo3 := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . Descr_Vo3 (31b02.. x0 x1)
Theorem 9bae8.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → ((ι → ο) → ο) → ο . (∀ x3 . In x3 x1 ⟶ 31b02.. x0 x3 (x2 x3)) ⟶ 31b02.. x0 x1 (x0 x1 x2)
Theorem 8ac8a.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ((ι → ο) → ο) → ο . 31b02.. x0 x1 x2 ⟶ ∃ x3 : ι → ((ι → ο) → ο) → ο . and (∀ x5 . In x5 x1 ⟶ 31b02.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Theorem e33bc.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ((ι → ο) → ο) → ο . 31b02.. x0 x1 x2 ⟶ 31b02.. x0 x1 x3 ⟶ x2 = x3
Theorem b5998.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 31b02.. x0 x1 (2bbaf.. x0 x1)
Theorem 9f3e1.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 31b02.. x0 x1 (x0 x1 (2bbaf.. x0))
Theorem 32d2e..^{In_rec_Vo3_eq} : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 2bbaf.. x0 x1 = x0 x1 (2bbaf.. x0)
Definition 77406.. := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . λ x2 : (((ι → ο) → ο) → ο) → ο . ∀ x3 : ι → ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition 59fb5..^In_rec_Vo4 := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . Descr_Vo4 (77406.. x0 x1)
Theorem 57125.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x3 . In x3 x1 ⟶ 77406.. x0 x3 (x2 x3)) ⟶ 77406.. x0 x1 (x0 x1 x2)
Theorem a7e02.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : (((ι → ο) → ο) → ο) → ο . 77406.. x0 x1 x2 ⟶ ∃ x3 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . In x5 x1 ⟶ 77406.. x0 x5 (x3 x5)) (x2 = x0 x1 x3)
Theorem 6dbd6.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (((ι → ο) → ο) → ο) → ο . 77406.. x0 x1 x2 ⟶ 77406.. x0 x1 x3 ⟶ x2 = x3
Theorem 8a2fc.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 77406.. x0 x1 (59fb5.. x0 x1)
Theorem 6fbc8.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 77406.. x0 x1 (x0 x1 (59fb5.. x0))
Theorem c6e41..^{In_rec_Vo4_eq} : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 59fb5.. x0 x1 = x0 x1 (59fb5.. x0)
Definition 1ce4f..^incl_0_1 := λ x0 x1 . In x1 x0
Definition d97e3..^In_1 := λ x0 x1 : ι → ο . ∃ x2 . and (x0 = 1ce4f.. x2) (x1 x2)
Definition 407b5..^incl_1_2 := λ x0 x1 : ι → ο . d97e3.. x1 x0
Definition 3a6d0..^In_2 := λ x0 x1 : (ι → ο) → ο . ∃ x2 : ι → ο . and (x0 = 407b5.. x2) (x1 x2)
Definition a4b00..^incl_2_3 := λ x0 x1 : (ι → ο) → ο . 3a6d0.. x1 x0
Definition e6217..^In_3 := λ x0 x1 : ((ι → ο) → ο) → ο . ∃ x2 : (ι → ο) → ο . and (x0 = a4b00.. x2) (x1 x2)
Definition a327b..^incl_3_4 := λ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x1 x0
Definition 8fddf..^In_4 := λ x0 x1 : (((ι → ο) → ο) → ο) → ο . ∃ x2 : ((ι → ο) → ο) → ο . and (x0 = a327b.. x2) (x1 x2)
Theorem 289f7..^In_1_I : ∀ x0 . ∀ x1 : ι → ο . x1 x0 ⟶ d97e3.. (1ce4f.. x0) x1
Theorem 4487e..^In_1_E : ∀ x0 x1 : ι → ο . d97e3.. x0 x1 ⟶ ∀ x2 : (ι → ο) → ο . (∀ x3 . x1 x3 ⟶ x2 (1ce4f.. x3)) ⟶ x2 x0
Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
Theorem c0781..^incl_0_1_inj : ∀ x0 x1 . 1ce4f.. x0 = 1ce4f.. x1 ⟶ x0 = x1
Theorem 8bd78..^In_1_up : ∀ x0 x1 . In x0 x1 ⟶ d97e3.. (1ce4f.. x0) (1ce4f.. x1)
Theorem 3172a..^In_1_down : ∀ x0 x1 . d97e3.. (1ce4f.. x0) (1ce4f.. x1) ⟶ In x0 x1
Theorem 5b9f0..^In_2_I : ∀ x0 : ι → ο . ∀ x1 : (ι → ο) → ο . x1 x0 ⟶ 3a6d0.. (407b5.. x0) x1
Theorem 724a1..^In_2_E : ∀ x0 x1 : (ι → ο) → ο . 3a6d0.. x0 x1 ⟶ ∀ x2 : ((ι → ο) → ο) → ο . (∀ x3 : ι → ο . x1 x3 ⟶ x2 (407b5.. x3)) ⟶ x2 x0
Theorem 94a3d..^incl_1_2_inj : ∀ x0 x1 : ι → ο . 407b5.. x0 = 407b5.. x1 ⟶ x0 = x1
Theorem 9b744..^In_2_up : ∀ x0 x1 : ι → ο . d97e3.. x0 x1 ⟶ 3a6d0.. (407b5.. x0) (407b5.. x1)
Theorem d6cc7..^In_2_down : ∀ x0 x1 : ι → ο . 3a6d0.. (407b5.. x0) (407b5.. x1) ⟶ d97e3.. x0 x1
Theorem 7abdf..^In_3_I : ∀ x0 : (ι → ο) → ο . ∀ x1 : ((ι → ο) → ο) → ο . x1 x0 ⟶ e6217.. (a4b00.. x0) x1
Theorem af1a5..^In_3_E : ∀ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x0 x1 ⟶ ∀ x2 : (((ι → ο) → ο) → ο) → ο . (∀ x3 : (ι → ο) → ο . x1 x3 ⟶ x2 (a4b00.. x3)) ⟶ x2 x0
Theorem ea98f..^incl_2_3_inj : ∀ x0 x1 : (ι → ο) → ο . a4b00.. x0 = a4b00.. x1 ⟶ x0 = x1
Theorem 37ad7..^In_3_up : ∀ x0 x1 : (ι → ο) → ο . 3a6d0.. x0 x1 ⟶ e6217.. (a4b00.. x0) (a4b00.. x1)
Theorem db604..^In_3_down : ∀ x0 x1 : (ι → ο) → ο . e6217.. (a4b00.. x0) (a4b00.. x1) ⟶ 3a6d0.. x0 x1
Theorem 483c0..^In_4_I : ∀ x0 : ((ι → ο) → ο) → ο . ∀ x1 : (((ι → ο) → ο) → ο) → ο . x1 x0 ⟶ 8fddf.. (a327b.. x0) x1
Theorem 272c7..^In_4_E : ∀ x0 x1 : (((ι → ο) → ο) → ο) → ο . 8fddf.. x0 x1 ⟶ ∀ x2 : ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x3 : ((ι → ο) → ο) → ο . x1 x3 ⟶ x2 (a327b.. x3)) ⟶ x2 x0
Theorem 79850..^incl_3_4_inj : ∀ x0 x1 : ((ι → ο) → ο) → ο . a327b.. x0 = a327b.. x1 ⟶ x0 = x1
Theorem b7736..^In_4_up : ∀ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x0 x1 ⟶ 8fddf.. (a327b.. x0) (a327b.. x1)
Theorem edf38..^In_4_down : ∀ x0 x1 : ((ι → ο) → ο) → ο . 8fddf.. (a327b.. x0) (a327b.. x1) ⟶ e6217.. x0 x1