Proofgold Asset

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Known In_0_2^In_0_2 : 0 ∈ 2
Known In_1_2^In_1_2 : 1 ∈ 2
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known neq_1_0^neq_1_0 : 1 = 0 ⟶ ∀ x0 : ο . x0
Theorem ad7a7.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ ∀ x9 . x9 ⊆ x8 ⟶ atleastp 2 x9 ⟶ ∀ x10 : ο . (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ x10 (proof)
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known In_2_3^In_2_3 : 2 ∈ 3
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Param nat_p^nat_p : ι → ο
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known nat_3^nat_3 : nat_p 3
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Theorem a6a5a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ ∀ x9 . x9 ⊆ x8 ⟶ atleastp 3 x9 ⟶ ∀ x10 : ο . (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ x10 (proof)
Known In_3_4^In_3_4 : 3 ∈ 4
Known nat_4^nat_4 : nat_p 4
Theorem c14f6.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ ∀ x9 . x9 ⊆ x8 ⟶ atleastp 4 x9 ⟶ ∀ x10 : ο . (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ x10 (proof)