satffunlem2lem1

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

Proof

Step	Hyp	Ref	Expression
1		satffunlem2lem1.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2		satffunlem2lem1.a	⊢ 𝐴 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
3		satffunlem2lem1.b	⊢ 𝐵 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
4		simpl	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → 𝑢 = 𝑠 )
5	4	fveq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) )
6		simpr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → 𝑣 = 𝑟 )
7	6	fveq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) )
8	5 7	oveq12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) )
9	8	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ) )
10	4	fveq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
11	6	fveq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ 𝑟 ) )
12	10 11	ineq12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) = ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) )
13	12	difeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) )
14	2 13	eqtrid	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → 𝐴 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) )
15	14	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑦 = 𝐴 ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
16	9 15	anbi12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
17	16	cbvrexdva	⊢ ( 𝑢 = 𝑠 → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
18		simpr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → 𝑖 = 𝑗 )
19		fveq2	⊢ ( 𝑢 = 𝑠 → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) )
20	19	adantr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) )
21	18 20	goaleq12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) )
22	21	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ) )
23	3	eqeq2i	⊢ ( 𝑦 = 𝐵 ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } )
24		opeq1	⊢ ( 𝑖 = 𝑗 → ⟨ 𝑖 , 𝑧 ⟩ = ⟨ 𝑗 , 𝑧 ⟩ )
25	24	sneqd	⊢ ( 𝑖 = 𝑗 → { ⟨ 𝑖 , 𝑧 ⟩ } = { ⟨ 𝑗 , 𝑧 ⟩ } )
26		sneq	⊢ ( 𝑖 = 𝑗 → { 𝑖 } = { 𝑗 } )
27	26	difeq2d	⊢ ( 𝑖 = 𝑗 → ( ω ∖ { 𝑖 } ) = ( ω ∖ { 𝑗 } ) )
28	27	reseq2d	⊢ ( 𝑖 = 𝑗 → ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) = ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) )
29	25 28	uneq12d	⊢ ( 𝑖 = 𝑗 → ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) = ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) )
30	29	adantl	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) = ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) )
31		fveq2	⊢ ( 𝑢 = 𝑠 → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
32	31	adantr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
33	30 32	eleq12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ↔ ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ) )
34	33	ralbidv	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ↔ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ) )
35	34	rabbidv	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } )
36	35	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) )
37	23 36	bitrid	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 𝑦 = 𝐵 ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) )
38	22 37	anbi12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) )
39	38	cbvrexdva	⊢ ( 𝑢 = 𝑠 → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) )
40	17 39	orbi12d	⊢ ( 𝑢 = 𝑠 → ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) ) )
41	40	cbvrexvw	⊢ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ∃ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) )
42		fveq2	⊢ ( 𝑣 = 𝑟 → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) )
43	19 42	oveqan12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) )
44	43	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ) )
45	2	eqeq2i	⊢ ( 𝑦 = 𝐴 ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
46		fveq2	⊢ ( 𝑣 = 𝑟 → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ 𝑟 ) )
47	31 46	ineqan12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) = ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) )
48	47	difeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) )
49	48	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
50	45 49	bitrid	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑦 = 𝐴 ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
51	44 50	anbi12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
52	51	cbvrexdva	⊢ ( 𝑢 = 𝑠 → ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
53	52	cbvrexvw	⊢ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
54	41 53	orbi12i	⊢ ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑠 ) } ) ) ∨ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
55		simp-5l	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → Fun ( 𝑆 ‘ suc 𝑁 ) )
56		eldifi	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) )
57	56	adantl	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) )
58	57	anim1i	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
59	58	ad2antrr	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
60		eldifi	⊢ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) )
61	60	adantl	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) )
62	61	anim1i	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
63	55 59 62	3jca	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) )
64		id	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
65	2	eqeq2i	⊢ ( 𝑤 = 𝐴 ↔ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
66	65	biimpi	⊢ ( 𝑤 = 𝐴 → 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
67	66	anim2i	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
68		satffunlem	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → 𝑦 = 𝑤 )
69	63 64 67 68	syl3an	⊢ ( ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 )
70	69	3exp	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
71	70	com23	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
72	71	rexlimdva	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
73		eqeq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
74		fvex	⊢ ( 1^st ‘ 𝑠 ) ∈ V
75		fvex	⊢ ( 1^st ‘ 𝑟 ) ∈ V
76		gonafv	⊢ ( ( ( 1^st ‘ 𝑠 ) ∈ V ∧ ( 1^st ‘ 𝑟 ) ∈ V ) → ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ )
77	74 75 76	mp2an	⊢ ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩
78		df-goal	⊢ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩
79	77 78	eqeq12i	⊢ ( ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ )
80		1oex	⊢ 1_o ∈ V
81		opex	⊢ ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ∈ V
82	80 81	opth	⊢ ( ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ ↔ ( 1_o = 2_o ∧ ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ = ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ) )
83		1one2o	⊢ 1_o ≠ 2_o
84		df-ne	⊢ ( 1_o ≠ 2_o ↔ ¬ 1_o = 2_o )
85		pm2.21	⊢ ( ¬ 1_o = 2_o → ( 1_o = 2_o → 𝑦 = 𝑤 ) )
86	84 85	sylbi	⊢ ( 1_o ≠ 2_o → ( 1_o = 2_o → 𝑦 = 𝑤 ) )
87	83 86	ax-mp	⊢ ( 1_o = 2_o → 𝑦 = 𝑤 )
88	87	adantr	⊢ ( ( 1_o = 2_o ∧ ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ = ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ) → 𝑦 = 𝑤 )
89	82 88	sylbi	⊢ ( ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ → 𝑦 = 𝑤 )
90	79 89	sylbi	⊢ ( ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → 𝑦 = 𝑤 )
91	73 90	biimtrdi	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → 𝑦 = 𝑤 ) )
92	91	adantr	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → 𝑦 = 𝑤 ) )
93	92	com12	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) )
94	93	adantr	⊢ ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) )
95	94	a1i	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
96	95	rexlimdva	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
97	72 96	jaod	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
98	97	rexlimdva	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
99		simp-4l	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → Fun ( 𝑆 ‘ suc 𝑁 ) )
100	58	adantr	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
101		ssel	⊢ ( ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) → ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
102	101	ad3antlr	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
103	102	com12	⊢ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) → ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
104	103	adantr	⊢ ( ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
105	104	impcom	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) )
106		eldifi	⊢ ( 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) )
107	106	ad2antll	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) )
108	105 107	jca	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
109	99 100 108	3jca	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) )
110	109 64 67 68	syl3an	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 )
111	110	3exp	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
112	111	com23	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
113	112	rexlimdvva	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
114	98 113	jaod	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑤 ) ) )
115	114	com23	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
116	115	rexlimdva	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
117		eqeq1	⊢ ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
118		df-goal	⊢ ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩
119		fvex	⊢ ( 1^st ‘ 𝑢 ) ∈ V
120		fvex	⊢ ( 1^st ‘ 𝑣 ) ∈ V
121		gonafv	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ V ∧ ( 1^st ‘ 𝑣 ) ∈ V ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
122	119 120 121	mp2an	⊢ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩
123	118 122	eqeq12i	⊢ ( ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
124		2oex	⊢ 2_o ∈ V
125		opex	⊢ ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ∈ V
126	124 125	opth	⊢ ( ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ ↔ ( 2_o = 1_o ∧ ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ = ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ) )
127	87	eqcoms	⊢ ( 2_o = 1_o → 𝑦 = 𝑤 )
128	127	adantr	⊢ ( ( 2_o = 1_o ∧ ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ = ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ) → 𝑦 = 𝑤 )
129	126 128	sylbi	⊢ ( ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ → 𝑦 = 𝑤 )
130	123 129	sylbi	⊢ ( ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑦 = 𝑤 )
131	117 130	biimtrdi	⊢ ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑦 = 𝑤 ) )
132	131	adantr	⊢ ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑦 = 𝑤 ) )
133	132	com12	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) )
134	133	adantr	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) )
135	134	rexlimivw	⊢ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) )
136	135	a1i	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
137		eqeq1	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ) )
138	78 118	eqeq12i	⊢ ( ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ )
139		opex	⊢ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ∈ V
140	124 139	opth	⊢ ( ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ ↔ ( 2_o = 2_o ∧ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ) )
141		vex	⊢ 𝑖 ∈ V
142	141 119	opth	⊢ ( ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ↔ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) )
143	142	anbi2i	⊢ ( ( 2_o = 2_o ∧ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) )
144	138 140 143	3bitri	⊢ ( ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) )
145	137 144	bitrdi	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) ) )
146	145	adantl	⊢ ( ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) ) )
147	56	a1i	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
148		funfv1st2nd	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) )
149	148	ex	⊢ ( Fun ( 𝑆 ‘ suc 𝑁 ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) )
150	149	adantr	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) )
151		funfv1st2nd	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) )
152	151	ex	⊢ ( Fun ( 𝑆 ‘ suc 𝑁 ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ) )
153	152	adantr	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ) )
154		fveqeq2	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ↔ ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) ) )
155		eqtr2	⊢ ( ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
156	29	eqcomd	⊢ ( 𝑖 = 𝑗 → ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) = ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) )
157	156	adantl	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) = ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) )
158		simpl	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
159	158	eqcomd	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ 𝑢 ) )
160	157 159	eleq12d	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ↔ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ) )
161	160	ralbidv	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ↔ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ) )
162	161	rabbidv	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } )
163	162 3	eqtr4di	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } = 𝐵 )
164		eqeq12	⊢ ( ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ∧ 𝑤 = 𝐵 ) → ( 𝑦 = 𝑤 ↔ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } = 𝐵 ) )
165	163 164	syl5ibrcom	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ∧ 𝑤 = 𝐵 ) → 𝑦 = 𝑤 ) )
166	165	exp4b	⊢ ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
167	155 166	syl	⊢ ( ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
168	167	ex	⊢ ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) )
169	154 168	biimtrdi	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) ) )
170	169	com24	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) ) )
171	170	impcom	⊢ ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) )
172	171	com13	⊢ ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) )
173	60 153 172	syl56	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) ) )
174	173	com23	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ( 𝑆 ‘ suc 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) ) )
175	147 150 174	3syld	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) ) )
176	175	imp	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) )
177	176	adantr	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) ) )
178	177	imp	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
179	178	adantld	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
180	179	ad2antrr	⊢ ( ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
181	146 180	sylbid	⊢ ( ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
182	181	impd	⊢ ( ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) )
183	182	ex	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( 𝑤 = 𝐵 → 𝑦 = 𝑤 ) ) ) )
184	183	com34	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑤 = 𝐵 → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) ) )
185	184	impd	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
186	185	rexlimdva	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
187	136 186	jaod	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
188	187	rexlimdva	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
189	134	a1i	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
190	189	rexlimdva	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
191	190	rexlimdva	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
192	188 191	jaod	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑤 ) ) )
193	192	com23	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑗 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
194	193	rexlimdva	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
195	116 194	jaod	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
196	195	rexlimdva	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
197		simplll	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) → Fun ( 𝑆 ‘ suc 𝑁 ) )
198		ssel	⊢ ( ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) → ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
199	198	adantrd	⊢ ( ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) → ( ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
200	199	adantl	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
201	200	imp	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) )
202		eldifi	⊢ ( 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) )
203	202	ad2antll	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) )
204	201 203	jca	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
205	204	adantr	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
206	60	anim1i	⊢ ( ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
207	206	adantl	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
208	197 205 207	3jca	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) → ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) )
209	208	adantr	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) ∧ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) )
210		simprl	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) ∧ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
211	67	ad2antll	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) ∧ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
212	209 210 211 68	syl3anc	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) ∧ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → 𝑦 = 𝑤 )
213	212	exp32	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
214	213	impancom	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → ( ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
215	214	expdimp	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
216	215	rexlimdv	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) )
217	91	adantrd	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → 𝑦 = 𝑤 ) )
218	217	adantr	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → 𝑦 = 𝑤 ) )
219	218	ad3antlr	⊢ ( ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → 𝑦 = 𝑤 ) )
220	219	rexlimdva	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) → 𝑦 = 𝑤 ) )
221	216 220	jaod	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) → 𝑦 = 𝑤 ) )
222	221	rexlimdva	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) → 𝑦 = 𝑤 ) )
223		simplll	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → Fun ( 𝑆 ‘ suc 𝑁 ) )
224	204	adantr	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
225	101	adantl	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
226	225	adantr	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
227	226	com12	⊢ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) → ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
228	227	adantr	⊢ ( ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
229	228	impcom	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) )
230	106	ad2antll	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) )
231	229 230	jca	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) )
232	223 224 231	3jca	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ) )
233	232 64 67 68	syl3an	⊢ ( ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 )
234	233	3exp	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
235	234	impancom	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → ( ( 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) ) )
236	235	rexlimdvv	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) → 𝑦 = 𝑤 ) )
237	222 236	jaod	⊢ ( ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) )
238	237	ex	⊢ ( ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
239	238	rexlimdvva	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
240	196 239	jaod	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑠 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑟 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) ∨ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑟 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
241	54 240	biimtrid	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) → 𝑦 = 𝑤 ) ) )
242	241	impd	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → 𝑦 = 𝑤 ) )
243	242	alrimivv	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ∀ 𝑦 ∀ 𝑤 ( ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → 𝑦 = 𝑤 ) )
244		eqeq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 = 𝐴 ↔ 𝑤 = 𝐴 ) )
245	244	anbi2d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) )
246	245	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) )
247		eqeq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 = 𝐵 ↔ 𝑤 = 𝐵 ) )
248	247	anbi2d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) )
249	248	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) )
250	246 249	orbi12d	⊢ ( 𝑦 = 𝑤 → ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ) )
251	250	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ↔ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ) )
252	245	2rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) )
253	251 252	orbi12d	⊢ ( 𝑦 = 𝑤 → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) )
254	253	mo4	⊢ ( ∃* 𝑦 ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) ∧ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑤 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = 𝐴 ) ) ) → 𝑦 = 𝑤 ) )
255	243 254	sylibr	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ∃* 𝑦 ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
256	255	alrimiv	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → ∀ 𝑥 ∃* 𝑦 ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
257		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ 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 ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) )
258	256 257	sylibr	⊢ ( ( Fun ( 𝑆 ‘ suc 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } )

Metamath Proof Explorer

Theorem satffunlem2lem1

Proof