Metamath Proof Explorer


Theorem satffunlem2lem1

Description: Lemma 1 for satffunlem2 . (Contributed by AV, 28-Oct-2023)

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

Proof

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