satfvsucsuc

Description: The satisfaction predicate as function over wff codes of height ( N + 1 ) , expressed by the minimally necessary satisfaction predicates as function over wff codes of height N . (Contributed by AV, 21-Oct-2023)

	Ref	Expression
Hypotheses	satfvsucsuc.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
	satfvsucsuc.a	⊢ 𝐴 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
	satfvsucsuc.b	⊢ 𝐵 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
Assertion	satfvsucsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑆 ‘ suc suc 𝑁 ) = ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		satfvsucsuc.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2		satfvsucsuc.a	⊢ 𝐴 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
3		satfvsucsuc.b	⊢ 𝐵 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
4		peano2	⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
5	1	satfvsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) → ( 𝑆 ‘ suc suc 𝑁 ) = ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
6	4 5	syl3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑆 ‘ suc suc 𝑁 ) = ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
7		orc	⊢ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
8	7	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
9	2	eqeq2i	⊢ ( 𝑦 = 𝐴 ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
10	9	anbi2i	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
11	10	rexbii	⊢ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
12	3	eqeq2i	⊢ ( 𝑦 = 𝐵 ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } )
13	12	anbi2i	⊢ ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
14	13	rexbii	⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
15	11 14	orbi12i	⊢ ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
16	15	rexbii	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
17	16	bicomi	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
18		3simpa	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) )
19	4	ancri	⊢ ( 𝑁 ∈ ω → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) )
20	19	3ad2ant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) )
21	18 20	jca	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) )
22		sssucid	⊢ 𝑁 ⊆ suc 𝑁
23	22	a1i	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑁 ⊆ suc 𝑁 )
24	1	satfsschain	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) → ( 𝑁 ⊆ suc 𝑁 → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) )
25	24	imp	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) ∧ 𝑁 ⊆ suc 𝑁 ) → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) )
26	21 23 25	syl2an2r	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) )
27		undif	⊢ ( ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ↔ ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) = ( 𝑆 ‘ suc 𝑁 ) )
28	26 27	sylib	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) = ( 𝑆 ‘ suc 𝑁 ) )
29	28	eqcomd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑆 ‘ suc 𝑁 ) = ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) )
30	29	rexeqdv	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ∃ 𝑢 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
31		rexun	⊢ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
32	30 31	bitrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) ) )
33	17 32	bitrid	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) ) )
34		r19.43	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
35	22	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → 𝑁 ⊆ suc 𝑁 )
36	21 35	jca	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) ∧ 𝑁 ⊆ suc 𝑁 ) )
37	36 25	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) )
38	37	adantr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) )
39	38 27	sylib	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) = ( 𝑆 ‘ suc 𝑁 ) )
40	39	eqcomd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑆 ‘ suc 𝑁 ) = ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) )
41	40	rexeqdv	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑣 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
42		rexun	⊢ ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
43	41 42	bitrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
44	43	rexbidv	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
45	44	orbi1d	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
46		r19.43	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
47	46	orbi1i	⊢ ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
48		or32	⊢ ( ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
49		r19.43	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
50	49	bicomi	⊢ ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
51	50	orbi1i	⊢ ( ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
52	48 51	bitri	⊢ ( ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
53	47 52	bitri	⊢ ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
54	45 53	bitrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
55	34 54	bitrid	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
56		animorr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
57	1	satfvsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑆 ‘ suc 𝑁 ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
58	57	eleq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ↔ 𝑠 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) )
59	58	adantr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ↔ 𝑠 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) )
60		eleq1	⊢ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) )
61	60	adantl	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) )
62		elun	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
63		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
64	63	orbi2i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
65	62 64	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
66	61 65	bitrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
67	59 66	bitrd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
68	2	eqcomi	⊢ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = 𝐴
69	68	eqeq2i	⊢ ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ↔ 𝑦 = 𝐴 )
70	69	anbi2i	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) )
71	70	rexbii	⊢ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) )
72	3	eqcomi	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = 𝐵
73	72	eqeq2i	⊢ ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ↔ 𝑦 = 𝐵 )
74	73	anbi2i	⊢ ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) )
75	74	rexbii	⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) )
76	71 75	orbi12i	⊢ ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
77	76	rexbii	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
78	77	a1i	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
79	78	orbi2d	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) ) )
80	67 79	bitrd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) ) )
81	80	adantr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) ) )
82	56 81	mpbird	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) )
83	82	orcd	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
84	83	ex	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
85		simplr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ )
86		animorr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
87	85 86	jca	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
88	87	olcd	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
89	88	ex	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
90	84 89	jaod	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
91	55 90	sylbid	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
92		simplr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ )
93		orc	⊢ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
94	93	adantl	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
95	92 94	jca	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
96	95	olcd	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
97	96	ex	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
98	91 97	jaod	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
99	33 98	sylbid	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
100	99	expimpd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
101	100	2eximdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
102		19.45v	⊢ ( ∃ 𝑦 ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
103	102	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ↔ ∃ 𝑥 ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
104		19.45v	⊢ ( ∃ 𝑥 ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
105	103 104	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
106	101 105	imbitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
107	8 106	jaod	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
108		difss	⊢ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ⊆ ( 𝑆 ‘ suc 𝑁 )
109		ssrexv	⊢ ( ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ⊆ ( 𝑆 ‘ suc 𝑁 ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
110	108 109	ax-mp	⊢ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) )
111	110	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ) )
112	111 16	imbitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
113		ssrexv	⊢ ( ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
114	37 113	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
115	10	2rexbii	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
116	114 115	imbitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
117	116	imp	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
118		ssrexv	⊢ ( ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ⊆ ( 𝑆 ‘ suc 𝑁 ) → ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
119	108 118	ax-mp	⊢ ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
120	119	reximi	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
121	117 120	syl	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
122	121	orcd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
123	122	ex	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
124		r19.43	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
125	123 124	imbitrrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
126	112 125	jaod	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
127	126	anim2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) → ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
128	127	2eximdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
129	128	orim2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) ) )
130	107 129	impbid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) ) )
131		elun	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ 𝑠 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
132		elopab	⊢ ( 𝑠 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
133	132	orbi2i	⊢ ( ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ 𝑠 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
134	131 133	bitri	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
135		elun	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ 𝑠 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) )
136		elopab	⊢ ( 𝑠 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) )
137	136	orbi2i	⊢ ( ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ 𝑠 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
138	135 137	bitri	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) ↔ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ) ) )
139	130 134 138	3bitr4g	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) ) )
140	139	eqrdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) )
141	6 140	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑆 ‘ suc suc 𝑁 ) = ( ( 𝑆 ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) )

Metamath Proof Explorer

Theorem satfvsucsuc

Proof