Metamath Proof Explorer

Theorem grothprim

Description: The Tarski-Grothendieck Axiom ax-groth expanded into set theory primitives using 163 symbols (allowing the defined symbols /\ , \/ , <-> , and E. ). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007)

Ref Expression
Assertion grothprim ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 axgroth4 ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
2 3anass ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
3 dfss2 ⊢ ( 𝑤 ⊆ 𝑧 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) )
4 elin ⊢ ( 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) )
5 3 4 imbi12i ⊢ ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) )
6 5 albii ⊢ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) )
7 6 rexbii ⊢ ( ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) )
8 df-rex ⊢ ( ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) )
9 7 8 bitri ⊢ ( ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) )
10 9 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) )
11 df-ral ⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) )
12 10 11 bitri ⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) )
13 dfss2 ⊢ ( 𝑧 ⊆ 𝑦 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) )
14 vex ⊢ 𝑦 ∈ V
15 14 difexi ⊢ ( 𝑦 ∖ 𝑧 ) ∈ V
16 vex ⊢ 𝑧 ∈ V
17 incom ⊢ ( ( 𝑦 ∖ 𝑧 ) ∩ 𝑧 ) = ( 𝑧 ∩ ( 𝑦 ∖ 𝑧 ) )
18 disjdif ⊢ ( 𝑧 ∩ ( 𝑦 ∖ 𝑧 ) ) = ∅
19 17 18 eqtri ⊢ ( ( 𝑦 ∖ 𝑧 ) ∩ 𝑧 ) = ∅
20 15 16 19 brdom6disj ⊢ ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ↔ ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) )
21 20 orbi1i ⊢ ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) )
22 19.44v ⊢ ( ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) )
23 21 22 bitr4i ⊢ ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) )
24 13 23 imbi12i ⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) )
25 19.35 ⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) )
26 24 25 bitr4i ⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) )
27 grothprimlem ⊢ ( { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) )
28 27 mobii ⊢ ( ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) )
29 df-mo ⊢ ( ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
30 28 29 bitri ⊢ ( ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
31 30 ralbii ⊢ ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∀ 𝑣 ∈ 𝑧 ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
32 df-ral ⊢ ( ∀ 𝑣 ∈ 𝑧 ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) )
33 31 32 bitri ⊢ ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) )
34 df-ral ⊢ ( ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) )
35 eldif ⊢ ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ↔ ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) )
36 grothprimlem ⊢ ( { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )
37 36 rexbii ⊢ ( ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑢 ∈ 𝑧 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )
38 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑧 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) )
39 37 38 bitri ⊢ ( ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) )
40 35 39 imbi12i ⊢ ( ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) → ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) )
41 pm5.6 ⊢ ( ( ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) → ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ↔ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
42 40 41 bitri ⊢ ( ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
43 42 albii ⊢ ( ∀ 𝑣 ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
44 34 43 bitri ⊢ ( ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
45 33 44 anbi12i ⊢ ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) )
46 19.26 ⊢ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ↔ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) )
47 45 46 bitr4i ⊢ ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) )
48 47 orbi1i ⊢ ( ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) )
49 48 imbi2i ⊢ ( ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
50 49 exbii ⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
51 26 50 bitri ⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
52 51 albii ⊢ ( ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
53 12 52 anbi12i ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )
54 19.26 ⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )
55 53 54 bitr4i ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )
56 55 anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
57 2 56 bitri ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
58 57 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
59 1 58 mpbi ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )