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		dfmo	⊢ ( ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) )
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	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) )