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

Metamath Proof Explorer

Theorem fmla1

Description: The valid Godel formulas of height 1 is the set of all formulas of the form ( a |g b ) and A.g k a with atoms a , b of the form x e. y . (Contributed by AV, 20-Sep-2023)

Ref Expression
Assertion fmla1 ( Fmla ‘ 1o ) = ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } )

Proof

Step Hyp Ref Expression
1 df-1o ⊢ 1o = suc ∅
2 1 fveq2i ⊢ ( Fmla ‘ 1o ) = ( Fmla ‘ suc ∅ )
3 peano1 ⊢ ∅ ∈ ω
4 fmlasuc ⊢ ( ∅ ∈ ω → ( Fmla ‘ suc ∅ ) = ( ( Fmla ‘ ∅ ) ∪ { 𝑥 ∣ ∃ 𝑝 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) } ) )
5 3 4 ax-mp ⊢ ( Fmla ‘ suc ∅ ) = ( ( Fmla ‘ ∅ ) ∪ { 𝑥 ∣ ∃ 𝑝 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) } )
6 fmla0xp ⊢ ( Fmla ‘ ∅ ) = ( { ∅ } × ( ω × ω ) )
7 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) }
8 7 rexeqi ⊢ ( ∃ 𝑝 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ↔ ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) )
9 eqeq1 ⊢ ( 𝑦 = 𝑝 → ( 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) ) )
10 9 2rexbidv ⊢ ( 𝑦 = 𝑝 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) ) )
11 10 elrab ⊢ ( 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ↔ ( 𝑝 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) ) )
12 oveq1 ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑝 ⊼𝑔 𝑞 ) = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) )
13 12 eqeq2d ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ↔ 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) ) )
14 13 rexbidv ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ↔ ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) ) )
15 eqidd ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → 𝑘 = 𝑘 )
16 id ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) )
17 15 16 goaleq12d ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ∀𝑔 𝑘 𝑝 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) )
18 17 eqeq2d ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑥 = ∀𝑔 𝑘 𝑝 ↔ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
19 18 rexbidv ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ↔ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
20 14 19 orbi12d ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ↔ ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
21 eqeq1 ⊢ ( 𝑧 = 𝑞 → ( 𝑧 = ( 𝑘 ∈𝑔 𝑙 ) ↔ 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) ) )
22 21 2rexbidv ⊢ ( 𝑧 = 𝑞 → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑧 = ( 𝑘 ∈𝑔 𝑙 ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) ) )
23 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑧 ∈ V ∣ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑧 = ( 𝑘 ∈𝑔 𝑙 ) }
24 22 23 elrab2 ⊢ ( 𝑞 ∈ ( Fmla ‘ ∅ ) ↔ ( 𝑞 ∈ V ∧ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) ) )
25 oveq2 ⊢ ( 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) → ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) )
26 25 eqeq2d ⊢ ( 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) ↔ 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
27 26 biimpcd ⊢ ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) → ( 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) → 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
28 27 reximdv ⊢ ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) → ( ∃ 𝑙 ∈ ω 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) → ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
29 28 reximdv ⊢ ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
30 29 com12 ⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑞 = ( 𝑘 ∈𝑔 𝑙 ) → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
31 24 30 simplbiim ⊢ ( 𝑞 ∈ ( Fmla ‘ ∅ ) → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
32 31 rexlimiv ⊢ ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) )
33 32 orim1i ⊢ ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
34 r19.43 ⊢ ( ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
35 33 34 sylibr ⊢ ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) → ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
36 20 35 biimtrdi ⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
37 36 com12 ⊢ ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
38 37 reximdv ⊢ ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ( ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
39 38 reximdv ⊢ ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
40 39 com12 ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
41 11 40 simplbiim ⊢ ( 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } → ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
42 41 rexlimiv ⊢ ( ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
43 oveq1 ⊢ ( 𝑖 = 𝑚 → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝑚 ∈𝑔 𝑗 ) )
44 43 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) )
45 44 eqeq2d ⊢ ( 𝑖 = 𝑚 → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
46 45 rexbidv ⊢ ( 𝑖 = 𝑚 → ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
47 eqidd ⊢ ( 𝑖 = 𝑚 → 𝑘 = 𝑘 )
48 47 43 goaleq12d ⊢ ( 𝑖 = 𝑚 → ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) )
49 48 eqeq2d ⊢ ( 𝑖 = 𝑚 → ( 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) ) )
50 46 49 orbi12d ⊢ ( 𝑖 = 𝑚 → ( ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) ) ) )
51 50 rexbidv ⊢ ( 𝑖 = 𝑚 → ( ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) ) ) )
52 oveq2 ⊢ ( 𝑗 = 𝑛 → ( 𝑚 ∈𝑔 𝑗 ) = ( 𝑚 ∈𝑔 𝑛 ) )
53 52 oveq1d ⊢ ( 𝑗 = 𝑛 → ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) )
54 53 eqeq2d ⊢ ( 𝑗 = 𝑛 → ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
55 54 rexbidv ⊢ ( 𝑗 = 𝑛 → ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
56 eqidd ⊢ ( 𝑗 = 𝑛 → 𝑘 = 𝑘 )
57 56 52 goaleq12d ⊢ ( 𝑗 = 𝑛 → ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) )
58 57 eqeq2d ⊢ ( 𝑗 = 𝑛 → ( 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) ↔ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) )
59 55 58 orbi12d ⊢ ( 𝑗 = 𝑛 → ( ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
60 59 rexbidv ⊢ ( 𝑗 = 𝑛 → ( ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
61 51 60 cbvrex2vw ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) )
62 oveq1 ⊢ ( 𝑘 = 𝑜 → ( 𝑘 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑙 ) )
63 62 oveq2d ⊢ ( 𝑘 = 𝑜 → ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) )
64 63 eqeq2d ⊢ ( 𝑘 = 𝑜 → ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) )
65 64 rexbidv ⊢ ( 𝑘 = 𝑜 → ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) )
66 id ⊢ ( 𝑘 = 𝑜 → 𝑘 = 𝑜 )
67 eqidd ⊢ ( 𝑘 = 𝑜 → ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑛 ) )
68 66 67 goaleq12d ⊢ ( 𝑘 = 𝑜 → ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) )
69 68 eqeq2d ⊢ ( 𝑘 = 𝑜 → ( 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ↔ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) )
70 65 69 orbi12d ⊢ ( 𝑘 = 𝑜 → ( ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ↔ ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
71 70 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑜 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) )
72 3 ne0ii ⊢ ω ≠ ∅
73 r19.44zv ⊢ ( ω ≠ ∅ → ( ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ↔ ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
74 72 73 ax-mp ⊢ ( ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ↔ ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) )
75 eqeq1 ⊢ ( 𝑦 = ( 𝑚 ∈𝑔 𝑛 ) → ( 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) ) )
76 75 2rexbidv ⊢ ( 𝑦 = ( 𝑚 ∈𝑔 𝑛 ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) ) )
77 ovexd ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) → ( 𝑚 ∈𝑔 𝑛 ) ∈ V )
78 simpl ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → 𝑚 ∈ ω )
79 43 eqeq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) ↔ ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑗 ) ) )
80 79 rexbidv ⊢ ( 𝑖 = 𝑚 → ( ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑗 ) ) )
81 80 adantl ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑖 = 𝑚 ) → ( ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑗 ) ) )
82 simpr ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → 𝑛 ∈ ω )
83 52 eqeq2d ⊢ ( 𝑗 = 𝑛 → ( ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑗 ) ↔ ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑛 ) ) )
84 83 adantl ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑗 = 𝑛 ) → ( ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑗 ) ↔ ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑛 ) ) )
85 eqidd ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑛 ) )
86 82 84 85 rspcedvd ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑚 ∈𝑔 𝑗 ) )
87 78 81 86 rspcedvd ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) )
88 87 ad3antrrr ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) )
89 76 77 88 elrabd ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) → ( 𝑚 ∈𝑔 𝑛 ) ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } )
90 oveq1 ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ( 𝑝 ⊼𝑔 𝑞 ) = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) )
91 90 eqeq2d ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ( 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ↔ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ) )
92 91 rexbidv ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ↔ ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ) )
93 eqidd ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → 𝑘 = 𝑘 )
94 id ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) )
95 93 94 goaleq12d ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ∀𝑔 𝑘 𝑝 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) )
96 95 eqeq2d ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ( 𝑥 = ∀𝑔 𝑘 𝑝 ↔ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) )
97 96 rexbidv ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ( ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ↔ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) )
98 92 97 orbi12d ⊢ ( 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) → ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ↔ ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
99 98 adantl ⊢ ( ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) ∧ 𝑝 = ( 𝑚 ∈𝑔 𝑛 ) ) → ( ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ↔ ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
100 ovexd ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( 𝑜 ∈𝑔 𝑙 ) ∈ V )
101 simpr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) → 𝑜 ∈ ω )
102 101 adantr ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → 𝑜 ∈ ω )
103 oveq1 ⊢ ( 𝑖 = 𝑜 → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝑜 ∈𝑔 𝑗 ) )
104 103 eqeq2d ⊢ ( 𝑖 = 𝑜 → ( ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) ↔ ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑗 ) ) )
105 104 rexbidv ⊢ ( 𝑖 = 𝑜 → ( ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑗 ) ) )
106 105 adantl ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑖 = 𝑜 ) → ( ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑗 ) ) )
107 simpr ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → 𝑙 ∈ ω )
108 oveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑜 ∈𝑔 𝑗 ) = ( 𝑜 ∈𝑔 𝑙 ) )
109 108 eqeq2d ⊢ ( 𝑗 = 𝑙 → ( ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑗 ) ↔ ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑙 ) ) )
110 109 adantl ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑗 = 𝑙 ) → ( ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑗 ) ↔ ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑙 ) ) )
111 eqidd ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑙 ) )
112 107 110 111 rspcedvd ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑜 ∈𝑔 𝑗 ) )
113 102 106 112 rspcedvd ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) )
114 eqeq1 ⊢ ( 𝑝 = ( 𝑜 ∈𝑔 𝑙 ) → ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) ) )
115 114 2rexbidv ⊢ ( 𝑝 = ( 𝑜 ∈𝑔 𝑙 ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) ) )
116 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑝 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) }
117 115 116 elrab2 ⊢ ( ( 𝑜 ∈𝑔 𝑙 ) ∈ ( Fmla ‘ ∅ ) ↔ ( ( 𝑜 ∈𝑔 𝑙 ) ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑜 ∈𝑔 𝑙 ) = ( 𝑖 ∈𝑔 𝑗 ) ) )
118 100 113 117 sylanbrc ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( 𝑜 ∈𝑔 𝑙 ) ∈ ( Fmla ‘ ∅ ) )
119 118 adantr ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) → ( 𝑜 ∈𝑔 𝑙 ) ∈ ( Fmla ‘ ∅ ) )
120 oveq2 ⊢ ( 𝑞 = ( 𝑜 ∈𝑔 𝑙 ) → ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) )
121 120 eqeq2d ⊢ ( 𝑞 = ( 𝑜 ∈𝑔 𝑙 ) → ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ↔ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) )
122 121 adantl ⊢ ( ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) ∧ 𝑞 = ( 𝑜 ∈𝑔 𝑙 ) ) → ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ↔ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) )
123 simpr ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) → 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) )
124 119 122 123 rspcedvd ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ) → ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) )
125 124 ex ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) → ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ) )
126 102 adantr ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → 𝑜 ∈ ω )
127 69 adantl ⊢ ( ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ∧ 𝑘 = 𝑜 ) → ( 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ↔ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) )
128 simpr ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) )
129 126 127 128 rspcedvd ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) )
130 129 ex ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) → ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) )
131 125 130 orim12d ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) ) )
132 131 imp ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) → ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) )
133 89 99 132 rspcedvd ⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) )
134 133 ex ⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) → ( ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
135 134 rexlimdva ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) → ( ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
136 74 135 biimtrrid ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) → ( ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
137 136 rexlimdva ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( ∃ 𝑜 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
138 71 137 biimtrid ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
139 138 rexlimivv ⊢ ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) )
140 61 139 sylbi ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) )
141 42 140 impbii ⊢ ( ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
142 8 141 bitri ⊢ ( ∃ 𝑝 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
143 142 abbii ⊢ { 𝑥 ∣ ∃ 𝑝 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) }
144 6 143 uneq12i ⊢ ( ( Fmla ‘ ∅ ) ∪ { 𝑥 ∣ ∃ 𝑝 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) } ) = ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } )
145 2 5 144 3eqtri ⊢ ( Fmla ‘ 1o ) = ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } )