This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 df-ss ⊢ ( 𝑤 ⊆ 𝑧 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) )
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 df-ss ⊢ ( 𝑧 ⊆ 𝑦 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) )
14 vex ⊢ 𝑦 ∈ V
15 14 difexi ⊢ ( 𝑦 ∖ 𝑧 ) ∈ V
16 vex ⊢ 𝑧 ∈ V
17 disjdifr ⊢ ( ( 𝑦 ∖ 𝑧 ) ∩ 𝑧 ) = ∅
18 15 16 17 brdom6disj ⊢ ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ↔ ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) )
19 18 orbi1i ⊢ ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) )
20 19.44v ⊢ ( ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) )
21 19 20 bitr4i ⊢ ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) )
22 13 21 imbi12i ⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) )
23 19.35 ⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) )
24 22 23 bitr4i ⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) )
25 grothprimlem ⊢ ( { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) )
26 25 mobii ⊢ ( ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) )
27 df-mo ⊢ ( ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
28 26 27 bitri ⊢ ( ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
29 28 ralbii ⊢ ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∀ 𝑣 ∈ 𝑧 ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
30 df-ral ⊢ ( ∀ 𝑣 ∈ 𝑧 ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) )
31 29 30 bitri ⊢ ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) )
32 df-ral ⊢ ( ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) )
33 eldif ⊢ ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ↔ ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) )
34 grothprimlem ⊢ ( { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )
35 34 rexbii ⊢ ( ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑢 ∈ 𝑧 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )
36 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑧 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) )
37 35 36 bitri ⊢ ( ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) )
38 33 37 imbi12i ⊢ ( ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) → ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) )
39 pm5.6 ⊢ ( ( ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) → ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ↔ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
40 38 39 bitri ⊢ ( ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
41 40 albii ⊢ ( ∀ 𝑣 ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
42 32 41 bitri ⊢ ( ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) )
43 31 42 anbi12i ⊢ ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) )
44 19.26 ⊢ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ↔ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) )
45 43 44 bitr4i ⊢ ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) )
46 45 orbi1i ⊢ ( ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) )
47 46 imbi2i ⊢ ( ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
48 47 exbii ⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
49 24 48 bitri ⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
50 49 albii ⊢ ( ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) )
51 12 50 anbi12i ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )
52 19.26 ⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )
53 51 52 bitr4i ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )
54 53 anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
55 2 54 bitri ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
56 55 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) )
57 1 56 mpbi ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )