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