satfv1

Description: The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023)

		Ref	Expression
	Hypothesis	satfv1.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
	Assertion	satfv1	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 1_o ) = ( ( 𝑆 ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		satfv1.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2		df-1o	⊢ 1_o = suc ∅
3	2	fveq2i	⊢ ( 𝑆 ‘ 1_o ) = ( 𝑆 ‘ suc ∅ )
4	3	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 1_o ) = ( 𝑆 ‘ suc ∅ ) )
5		peano1	⊢ ∅ ∈ ω
6	1	satfvsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω ) → ( 𝑆 ‘ suc ∅ ) = ( ( 𝑆 ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) } ) )
7	5 6	mp3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ suc ∅ ) = ( ( 𝑆 ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) } ) )
8	1	satfv0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ ∅ ) = { ⟨ 𝑒 , 𝑏 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } )
9	8	rexeqdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) ↔ ∃ 𝑜 ∈ { ⟨ 𝑒 , 𝑏 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) ) )
10		eqid	⊢ { ⟨ 𝑒 , 𝑏 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } = { ⟨ 𝑒 , 𝑏 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) }
11		vex	⊢ 𝑒 ∈ V
12		vex	⊢ 𝑏 ∈ V
13	11 12	op1std	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( 1^st ‘ 𝑜 ) = 𝑒 )
14	13	oveq1d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) )
15	14	eqeq2d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ↔ 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ) )
16	11 12	op2ndd	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( 2^nd ‘ 𝑜 ) = 𝑏 )
17	16	ineq1d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) = ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) )
18	17	difeq2d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) )
19	18	eqeq2d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) )
20	15 19	anbi12d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ↔ ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ) )
21	20	rexbidv	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ↔ ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ) )
22		eqidd	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → 𝑛 = 𝑛 )
23	22 13	goaleq12d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) = ∀_𝑔 𝑛 𝑒 )
24	23	eqeq2d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ↔ 𝑥 = ∀_𝑔 𝑛 𝑒 ) )
25	16	eleq2d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) ↔ ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 ) )
26	25	ralbidv	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) ↔ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 ) )
27	26	rabbidv	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } )
28	27	eqeq2d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) )
29	24 28	anbi12d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ↔ ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) )
30	29	rexbidv	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ↔ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) )
31	21 30	orbi12d	⊢ ( 𝑜 = ⟨ 𝑒 , 𝑏 ⟩ → ( ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) ↔ ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
32	10 31	rexopabb	⊢ ( ∃ 𝑜 ∈ { ⟨ 𝑒 , 𝑏 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) ↔ ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
33	9 32	bitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) ↔ ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ) )
34	1	satfv0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ ∅ ) = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) } )
35	34	rexeqdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ↔ ∃ 𝑝 ∈ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) } ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ) )
36		eqid	⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) }
37		vex	⊢ 𝑐 ∈ V
38		vex	⊢ 𝑑 ∈ V
39	37 38	op1std	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( 1^st ‘ 𝑝 ) = 𝑐 )
40	39	oveq2d	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) = ( 𝑒 ⊼_𝑔 𝑐 ) )
41	40	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ↔ 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ) )
42	37 38	op2ndd	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( 2^nd ‘ 𝑝 ) = 𝑑 )
43	42	ineq2d	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) = ( 𝑏 ∩ 𝑑 ) )
44	43	difeq2d	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) )
45	44	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) )
46	41 45	anbi12d	⊢ ( 𝑝 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ↔ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) )
47	36 46	rexopabb	⊢ ( ∃ 𝑝 ∈ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) } ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ↔ ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) )
48	35 47	bitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ↔ ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ) )
49	48	orbi1d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ↔ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
50	49	anbi2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ) )
51	50	2exbidv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ) )
52		r19.41vv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
53		oveq1	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑒 ⊼_𝑔 𝑐 ) = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) )
54	53	eqeq2d	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ↔ 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ) )
55		ineq1	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( 𝑏 ∩ 𝑑 ) = ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) )
56	55	difeq2d	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) )
57	56	eqeq2d	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) )
58	54 57	bi2anan9	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ↔ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
59	58	anbi2d	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ↔ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ) )
60	59	2exbidv	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ↔ ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ) )
61		eqidd	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → 𝑛 = 𝑛 )
62		id	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) )
63	61 62	goaleq12d	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → ∀_𝑔 𝑛 𝑒 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) )
64	63	eqeq2d	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑥 = ∀_𝑔 𝑛 𝑒 ↔ 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ) )
65		nfrab1	⊢ Ⅎ 𝑎 { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) }
66	65	nfeq2	⊢ Ⅎ 𝑎 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) }
67		eleq2	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 ↔ ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
68	67	ralbidv	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 ↔ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
69	66 68	rabbid	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } )
70	69	eqeq2d	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) )
71	64 70	bi2anan9	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ↔ ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) )
72	71	rexbidv	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ↔ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) )
73	60 72	orbi12d	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ↔ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) ) )
74	73	adantl	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → ( ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ↔ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) ) )
75		r19.41vv	⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ↔ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
76		oveq2	⊢ ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) → ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) )
77	76	adantr	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) )
78	77	eqeq2d	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ↔ 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ) )
79		ineq2	⊢ ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } → ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) = ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) )
80	79	difeq2d	⊢ ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } → ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) )
81		inrab	⊢ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∧ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) }
82	81	difeq2i	⊢ ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) = ( ( 𝑀 ↑_m ω ) ∖ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∧ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } )
83		notrab	⊢ ( ( 𝑀 ↑_m ω ) ∖ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∧ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ¬ ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∧ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) }
84		ianor	⊢ ( ¬ ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∧ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) )
85	84	rabbii	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ¬ ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∧ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) }
86	82 83 85	3eqtri	⊢ ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) }
87	80 86	eqtrdi	⊢ ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } → ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } )
88	87	eqeq2d	⊢ ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
89	88	adantl	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
90	78 89	anbi12d	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ↔ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
91	90	biimpa	⊢ ( ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) → ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
92	91	reximi	⊢ ( ∃ 𝑙 ∈ ω ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) → ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
93	92	reximi	⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
94	75 93	sylbir	⊢ ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
95	94	exlimivv	⊢ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
96	95	a1i	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
97		simpr	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → 𝑛 ∈ ω )
98		simpll	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → 𝑖 ∈ ω )
99		simplr	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → 𝑗 ∈ ω )
100		fveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ 𝑖 ) = ( 𝑏 ‘ 𝑖 ) )
101		fveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ 𝑗 ) = ( 𝑏 ‘ 𝑗 ) )
102	100 101	breq12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ( 𝑏 ‘ 𝑖 ) 𝐸 ( 𝑏 ‘ 𝑗 ) ) )
103	102	cbvrabv	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑏 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑏 ‘ 𝑖 ) 𝐸 ( 𝑏 ‘ 𝑗 ) }
104	103	eleq2i	⊢ ( ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑏 ‘ 𝑖 ) 𝐸 ( 𝑏 ‘ 𝑗 ) } )
105	104	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑏 ‘ 𝑖 ) 𝐸 ( 𝑏 ‘ 𝑗 ) } )
106	105	rabbii	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑏 ‘ 𝑖 ) 𝐸 ( 𝑏 ‘ 𝑗 ) } }
107		satfv1lem	⊢ ( ( 𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑏 ‘ 𝑖 ) 𝐸 ( 𝑏 ‘ 𝑗 ) } } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } )
108	106 107	eqtrid	⊢ ( ( 𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } )
109	97 98 99 108	syl3anc	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } )
110	109	eqeq2d	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) )
111	110	biimpd	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } → 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) )
112	111	anim2d	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) → ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
113	112	reximdva	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) → ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
114	113	adantr	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → ( ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) → ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
115	96 114	orim12d	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → ( ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
116	74 115	sylbid	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → ( ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
117	116	expimpd	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
118	117	reximdva	⊢ ( 𝑖 ∈ ω → ( ∃ 𝑗 ∈ ω ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) → ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
119	118	reximia	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
120	52 119	sylbir	⊢ ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
121	120	exlimivv	⊢ ( ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
122		ovex	⊢ ( 𝑖 ∈_𝑔 𝑗 ) ∈ V
123		ovex	⊢ ( 𝑀 ↑_m ω ) ∈ V
124	123	rabex	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∈ V
125	122 124	pm3.2i	⊢ ( ( 𝑖 ∈_𝑔 𝑗 ) ∈ V ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∈ V )
126		eqid	⊢ ( 𝑘 ∈_𝑔 𝑙 ) = ( 𝑘 ∈_𝑔 𝑙 )
127		eqid	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) }
128	126 127	pm3.2i	⊢ ( ( 𝑘 ∈_𝑔 𝑙 ) = ( 𝑘 ∈_𝑔 𝑙 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } )
129	86	eqcomi	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) )
130	129	eqeq2i	⊢ ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) )
131	130	biimpi	⊢ ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } → 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) )
132	131	anim2i	⊢ ( ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) → ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) ) )
133		ovex	⊢ ( 𝑘 ∈_𝑔 𝑙 ) ∈ V
134	123	rabex	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ∈ V
135		eqeq1	⊢ ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) → ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ↔ ( 𝑘 ∈_𝑔 𝑙 ) = ( 𝑘 ∈_𝑔 𝑙 ) ) )
136		eqeq1	⊢ ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } → ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ↔ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) )
137	135 136	bi2anan9	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ↔ ( ( 𝑘 ∈_𝑔 𝑙 ) = ( 𝑘 ∈_𝑔 𝑙 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) )
138	76	eqeq2d	⊢ ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) → ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ↔ 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ) )
139	80	eqeq2d	⊢ ( 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) ) )
140	138 139	bi2anan9	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ↔ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) ) ) )
141	137 140	anbi12d	⊢ ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) → ( ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ↔ ( ( ( 𝑘 ∈_𝑔 𝑙 ) = ( 𝑘 ∈_𝑔 𝑙 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) ) ) ) )
142	133 134 141	spc2ev	⊢ ( ( ( ( 𝑘 ∈_𝑔 𝑙 ) = ( 𝑘 ∈_𝑔 𝑙 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ) ) ) → ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
143	128 132 142	sylancr	⊢ ( ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) → ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
144	143	reximi	⊢ ( ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) → ∃ 𝑙 ∈ ω ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
145	144	reximi	⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
146	75	bicomi	⊢ ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
147	146	2exbii	⊢ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ↔ ∃ 𝑐 ∃ 𝑑 ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
148		2ex2rexrot	⊢ ( ∃ 𝑐 ∃ 𝑑 ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
149	147 148	bitri	⊢ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
150	145 149	sylibr	⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) → ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) )
151	150	a1i	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) → ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ) )
152	109	eqcomd	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } )
153	152	eqeq2d	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) )
154	153	biimpd	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } → 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) )
155	154	anim2d	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑛 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) → ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) )
156	155	reximdva	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) → ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) )
157	151 156	orim12d	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) → ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) ) )
158	157	imp	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) → ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) )
159		eqid	⊢ ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 )
160		eqid	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) }
161	159 160	pm3.2i	⊢ ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } )
162	158 161	jctil	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) → ( ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) ) )
163		eqeq1	⊢ ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) )
164		eqeq1	⊢ ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
165	163 164	bi2anan9	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
166	165 73	anbi12d	⊢ ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ( ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) ) ) )
167	166	spc2egv	⊢ ( ( ( 𝑖 ∈_𝑔 𝑗 ) ∈ V ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∈ V ) → ( ( ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } } ) ) ) → ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ) )
168	125 162 167	mpsyl	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) → ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
169	168	ex	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) → ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ) )
170	169	reximdva	⊢ ( 𝑖 ∈ ω → ( ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) → ∃ 𝑗 ∈ ω ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ) )
171	170	reximia	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
172	52	bicomi	⊢ ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
173	172	2exbii	⊢ ( ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑒 ∃ 𝑏 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
174		2ex2rexrot	⊢ ( ∃ 𝑒 ∃ 𝑏 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
175	173 174	bitri	⊢ ( ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑒 ∃ 𝑏 ( ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
176	171 175	sylibr	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) → ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) )
177	121 176	impbii	⊢ ( ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑐 ∃ 𝑑 ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑐 = ( 𝑘 ∈_𝑔 𝑙 ) ∧ 𝑑 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) } ) ∧ ( 𝑥 = ( 𝑒 ⊼_𝑔 𝑐 ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ 𝑑 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
178	51 177	bitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑒 ∃ 𝑏 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑒 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑏 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( 𝑒 ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( 𝑏 ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 𝑒 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ 𝑏 } ) ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
179	33 178	bitrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
180	179	opabbidv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } )
181	180	uneq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑆 ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑜 ∈ ( 𝑆 ‘ ∅ ) ( ∃ 𝑝 ∈ ( 𝑆 ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑜 ) ⊼_𝑔 ( 1^st ‘ 𝑝 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑜 ) ∩ ( 2^nd ‘ 𝑝 ) ) ) ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 1^st ‘ 𝑜 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑛 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑛 } ) ) ) ∈ ( 2^nd ‘ 𝑜 ) } ) ) } ) = ( ( 𝑆 ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )
182	4 7 181	3eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 1_o ) = ( ( 𝑆 ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈_𝑔 𝑗 ) ⊼_𝑔 ( 𝑘 ∈_𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀_𝑔 𝑛 ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )

Metamath Proof Explorer

Theorem satfv1

Proof