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	syl6bi	⊢ ( 𝑝 = ( 𝑖 ∈𝑔 𝑗 ) → ( ( ∃ 𝑞 ∈ ( 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	ad5ant12	⊢ ( ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) ∧ 𝑙 ∈ ω ) ∧ ( 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑚 ∈𝑔 𝑛 ) = ( 𝑖 ∈𝑔 𝑗 ) )
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	syl5bir	⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑜 ∈ ω ) → ( ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
137	136	rexlimdva	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( ∃ 𝑜 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑜 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑜 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖 ∈𝑔 𝑗 ) } ( ∃ 𝑞 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑝 ⊼𝑔 𝑞 ) ∨ ∃ 𝑘 ∈ ω 𝑥 = ∀𝑔 𝑘 𝑝 ) ) )
138	71 137	syl5bi	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑚 ∈𝑔 𝑛 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑚 ∈𝑔 𝑛 ) ) → ∃ 𝑝 ∈ { 𝑦 ∈ 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 ) = ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑙 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } )