Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  satffunlem2lem1 Structured version   Visualization version   GIF version

Theorem satffunlem2lem1 32736
Description: Lemma 1 for satffunlem2 32740. (Contributed by AV, 28-Oct-2023.)
Hypotheses
Ref Expression
satffunlem2lem1.s 𝑆 = (𝑀 Sat 𝐸)
satffunlem2lem1.a 𝐴 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
satffunlem2lem1.b 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
Assertion
Ref Expression
satffunlem2lem1 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))})
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑖,𝑀,𝑢   𝑣,𝑀,𝑢   𝑖,𝑁,𝑢,𝑥,𝑦   𝑣,𝑁,𝑥,𝑦   𝑆,𝑖,𝑢,𝑥,𝑦   𝑣,𝑆   𝑖,𝑎,𝑢   𝑣,𝑎   𝑧,𝑖,𝑢   𝑧,𝑣
Allowed substitution hints:   𝐴(𝑥,𝑧,𝑣,𝑢,𝑖,𝑎)   𝐵(𝑥,𝑧,𝑣,𝑢,𝑖,𝑎)   𝑆(𝑧,𝑎)   𝐸(𝑥,𝑦,𝑧,𝑣,𝑢,𝑖,𝑎)   𝑀(𝑥,𝑦,𝑧,𝑎)   𝑁(𝑧,𝑎)

Proof of Theorem satffunlem2lem1
Dummy variables 𝑗 𝑠 𝑤 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 486 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑣 = 𝑟) → 𝑢 = 𝑠)
21fveq2d 6667 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → (1st𝑢) = (1st𝑠))
3 simpr 488 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑣 = 𝑟) → 𝑣 = 𝑟)
43fveq2d 6667 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → (1st𝑣) = (1st𝑟))
52, 4oveq12d 7169 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑣 = 𝑟) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
65eqeq2d 2835 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))))
7 satffunlem2lem1.a . . . . . . . . . . . . . 14 𝐴 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
81fveq2d 6667 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑠𝑣 = 𝑟) → (2nd𝑢) = (2nd𝑠))
93fveq2d 6667 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑠𝑣 = 𝑟) → (2nd𝑣) = (2nd𝑟))
108, 9ineq12d 4175 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑣 = 𝑟) → ((2nd𝑢) ∩ (2nd𝑣)) = ((2nd𝑠) ∩ (2nd𝑟)))
1110difeq2d 4085 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))
127, 11syl5eq 2871 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑣 = 𝑟) → 𝐴 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))
1312eqeq2d 2835 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
146, 13anbi12d 633 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
1514cbvrexdva 3445 . . . . . . . . . 10 (𝑢 = 𝑠 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
16 simpr 488 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑖 = 𝑗) → 𝑖 = 𝑗)
17 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑢 = 𝑠 → (1st𝑢) = (1st𝑠))
1817adantr 484 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑖 = 𝑗) → (1st𝑢) = (1st𝑠))
1916, 18goaleq12d 32683 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑖 = 𝑗) → ∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠))
2019eqeq2d 2835 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑖 = 𝑗) → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ 𝑥 = ∀𝑔𝑗(1st𝑠)))
21 satffunlem2lem1.b . . . . . . . . . . . . . 14 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
2221eqeq2i 2837 . . . . . . . . . . . . 13 (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
23 opeq1 4787 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → ⟨𝑖, 𝑧⟩ = ⟨𝑗, 𝑧⟩)
2423sneqd 4562 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → {⟨𝑖, 𝑧⟩} = {⟨𝑗, 𝑧⟩})
25 sneq 4560 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑗 → {𝑖} = {𝑗})
2625difeq2d 4085 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (ω ∖ {𝑖}) = (ω ∖ {𝑗}))
2726reseq2d 5842 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑎 ↾ (ω ∖ {𝑖})) = (𝑎 ↾ (ω ∖ {𝑗})))
2824, 27uneq12d 4126 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))))
2928adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑢 = 𝑠𝑖 = 𝑗) → ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))))
30 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑠 → (2nd𝑢) = (2nd𝑠))
3130adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑢 = 𝑠𝑖 = 𝑗) → (2nd𝑢) = (2nd𝑠))
3229, 31eleq12d 2910 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑠𝑖 = 𝑗) → (({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢) ↔ ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)))
3332ralbidv 3192 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑖 = 𝑗) → (∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢) ↔ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)))
3433rabbidv 3465 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑖 = 𝑗) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})
3534eqeq2d 2835 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑖 = 𝑗) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}))
3622, 35syl5bb 286 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑖 = 𝑗) → (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}))
3720, 36anbi12d 633 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑖 = 𝑗) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})))
3837cbvrexdva 3445 . . . . . . . . . 10 (𝑢 = 𝑠 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})))
3915, 38orbi12d 916 . . . . . . . . 9 (𝑢 = 𝑠 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}))))
4039cbvrexvw 3435 . . . . . . . 8 (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})))
41 fveq2 6663 . . . . . . . . . . . . 13 (𝑣 = 𝑟 → (1st𝑣) = (1st𝑟))
4217, 41oveqan12d 7170 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
4342eqeq2d 2835 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))))
447eqeq2i 2837 . . . . . . . . . . . 12 (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
45 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑣 = 𝑟 → (2nd𝑣) = (2nd𝑟))
4630, 45ineqan12d 4176 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → ((2nd𝑢) ∩ (2nd𝑣)) = ((2nd𝑠) ∩ (2nd𝑟)))
4746difeq2d 4085 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))
4847eqeq2d 2835 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) ↔ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
4944, 48syl5bb 286 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
5043, 49anbi12d 633 . . . . . . . . . 10 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
5150cbvrexdva 3445 . . . . . . . . 9 (𝑢 = 𝑠 → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
5251cbvrexvw 3435 . . . . . . . 8 (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑠 ∈ (𝑆𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
5340, 52orbi12i 912 . . . . . . 7 ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})) ∨ ∃𝑠 ∈ (𝑆𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
54 simp-5l 784 . . . . . . . . . . . . . . . . . . . 20 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → Fun (𝑆‘suc 𝑁))
55 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁))
5655adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁))
5756anim1i 617 . . . . . . . . . . . . . . . . . . . . 21 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
5857ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
59 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁))
6059adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → 𝑢 ∈ (𝑆‘suc 𝑁))
6160anim1i 617 . . . . . . . . . . . . . . . . . . . 20 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
6254, 58, 613jca 1125 . . . . . . . . . . . . . . . . . . 19 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
63 id 22 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
647eqeq2i 2837 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝐴𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
6564biimpi 219 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝐴𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
6665anim2i 619 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
67 satffunlem 32733 . . . . . . . . . . . . . . . . . . 19 (((Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)
6862, 63, 66, 67syl3an 1157 . . . . . . . . . . . . . . . . . 18 (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
69683exp 1116 . . . . . . . . . . . . . . . . 17 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
7069com23 86 . . . . . . . . . . . . . . . 16 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
7170rexlimdva 3276 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
72 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ ((1st𝑠)⊼𝑔(1st𝑟)) = ∀𝑔𝑖(1st𝑢)))
73 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑠) ∈ V
74 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑟) ∈ V
75 gonafv 32682 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑠) ∈ V ∧ (1st𝑟) ∈ V) → ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
7673, 74, 75mp2an 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩
77 df-goal 32674 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔𝑖(1st𝑢) = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩
7876, 77eqeq12i 2839 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑠)⊼𝑔(1st𝑟)) = ∀𝑔𝑖(1st𝑢) ↔ ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩)
79 1oex 8108 . . . . . . . . . . . . . . . . . . . . . . . 24 1o ∈ V
80 opex 5344 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨(1st𝑠), (1st𝑟)⟩ ∈ V
8179, 80opth 5356 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ ↔ (1o = 2o ∧ ⟨(1st𝑠), (1st𝑟)⟩ = ⟨𝑖, (1st𝑢)⟩))
82 1one2o 8267 . . . . . . . . . . . . . . . . . . . . . . . . 25 1o ≠ 2o
83 df-ne 3015 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1o ≠ 2o ↔ ¬ 1o = 2o)
84 pm2.21 123 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ 1o = 2o → (1o = 2o𝑦 = 𝑤))
8583, 84sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1o ≠ 2o → (1o = 2o𝑦 = 𝑤))
8682, 85ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (1o = 2o𝑦 = 𝑤)
8786adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((1o = 2o ∧ ⟨(1st𝑠), (1st𝑟)⟩ = ⟨𝑖, (1st𝑢)⟩) → 𝑦 = 𝑤)
8881, 87sylbi 220 . . . . . . . . . . . . . . . . . . . . . 22 (⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ → 𝑦 = 𝑤)
8978, 88sylbi 220 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑠)⊼𝑔(1st𝑟)) = ∀𝑔𝑖(1st𝑢) → 𝑦 = 𝑤)
9072, 89syl6bi 256 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → (𝑥 = ∀𝑔𝑖(1st𝑢) → 𝑦 = 𝑤))
9190adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → (𝑥 = ∀𝑔𝑖(1st𝑢) → 𝑦 = 𝑤))
9291com12 32 . . . . . . . . . . . . . . . . . 18 (𝑥 = ∀𝑔𝑖(1st𝑢) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤))
9392adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤))
9493a1i 11 . . . . . . . . . . . . . . . 16 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
9594rexlimdva 3276 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
9671, 95jaod 856 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
9796rexlimdva 3276 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
98 simp-4l 782 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → Fun (𝑆‘suc 𝑁))
9957adantr 484 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
100 ssel 3946 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
101100ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
102101com12 32 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ (𝑆𝑁) → ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁)))
103102adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁)))
104103impcom 411 . . . . . . . . . . . . . . . . . . 19 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁))
105 eldifi 4089 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑣 ∈ (𝑆‘suc 𝑁))
106105ad2antll 728 . . . . . . . . . . . . . . . . . . 19 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁))
107104, 106jca 515 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
10898, 99, 1073jca 1125 . . . . . . . . . . . . . . . . 17 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
109108, 63, 66, 67syl3an 1157 . . . . . . . . . . . . . . . 16 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
1101093exp 1116 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
111110com23 86 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
112111rexlimdvva 3286 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
11397, 112jaod 856 . . . . . . . . . . . 12 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
114113com23 86 . . . . . . . . . . 11 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
115114rexlimdva 3276 . . . . . . . . . 10 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
116 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ∀𝑔𝑗(1st𝑠) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ∀𝑔𝑗(1st𝑠) = ((1st𝑢)⊼𝑔(1st𝑣))))
117 df-goal 32674 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔𝑗(1st𝑠) = ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩
118 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑢) ∈ V
119 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑣) ∈ V
120 gonafv 32682 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑢) ∈ V ∧ (1st𝑣) ∈ V) → ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
121118, 119, 120mp2an 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩
122117, 121eqeq12i 2839 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑔𝑗(1st𝑠) = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
123 2oex 8110 . . . . . . . . . . . . . . . . . . . . . . . 24 2o ∈ V
124 opex 5344 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗, (1st𝑠)⟩ ∈ V
125123, 124opth 5356 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ ↔ (2o = 1o ∧ ⟨𝑗, (1st𝑠)⟩ = ⟨(1st𝑢), (1st𝑣)⟩))
12686eqcoms 2832 . . . . . . . . . . . . . . . . . . . . . . . 24 (2o = 1o𝑦 = 𝑤)
127126adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((2o = 1o ∧ ⟨𝑗, (1st𝑠)⟩ = ⟨(1st𝑢), (1st𝑣)⟩) → 𝑦 = 𝑤)
128125, 127sylbi 220 . . . . . . . . . . . . . . . . . . . . . 22 (⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ → 𝑦 = 𝑤)
129122, 128sylbi 220 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑔𝑗(1st𝑠) = ((1st𝑢)⊼𝑔(1st𝑣)) → 𝑦 = 𝑤)
130116, 129syl6bi 256 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ∀𝑔𝑗(1st𝑠) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → 𝑦 = 𝑤))
131130adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → 𝑦 = 𝑤))
132131com12 32 . . . . . . . . . . . . . . . . . 18 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤))
133132adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤))
134133rexlimivw 3274 . . . . . . . . . . . . . . . 16 (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤))
135134a1i 11 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
136 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ∀𝑔𝑖(1st𝑢) → (𝑥 = ∀𝑔𝑗(1st𝑠) ↔ ∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠)))
13777, 117eqeq12i 2839 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠) ↔ ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ = ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩)
138 opex 5344 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖, (1st𝑢)⟩ ∈ V
139123, 138opth 5356 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ = ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, (1st𝑢)⟩ = ⟨𝑗, (1st𝑠)⟩))
140 vex 3483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑖 ∈ V
141140, 118opth 5356 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑖, (1st𝑢)⟩ = ⟨𝑗, (1st𝑠)⟩ ↔ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)))
142141anbi2i 625 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2o = 2o ∧ ⟨𝑖, (1st𝑢)⟩ = ⟨𝑗, (1st𝑠)⟩) ↔ (2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠))))
143137, 139, 1423bitri 300 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠) ↔ (2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠))))
144136, 143syl6bb 290 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ∀𝑔𝑖(1st𝑢) → (𝑥 = ∀𝑔𝑗(1st𝑠) ↔ (2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)))))
145144adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st𝑢)) → (𝑥 = ∀𝑔𝑗(1st𝑠) ↔ (2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)))))
14655a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁)))
147 funfv1st2nd 7742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun (𝑆‘suc 𝑁) ∧ 𝑠 ∈ (𝑆‘suc 𝑁)) → ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠))
148147ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠)))
149148adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠)))
150 funfv1st2nd 7742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Fun (𝑆‘suc 𝑁) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢))
151150ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Fun (𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢)))
152151adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢)))
153 fveqeq2 6672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st𝑢) = (1st𝑠) → (((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢) ↔ ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑢)))
154 eqtr2 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑢) ∧ ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠)) → (2nd𝑢) = (2nd𝑠))
15528eqcomd 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑖 = 𝑗 → ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))))
156155adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))))
157 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (2nd𝑢) = (2nd𝑠))
158157eqcomd 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (2nd𝑠) = (2nd𝑢))
159156, 158eleq12d 2910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠) ↔ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)))
160159ralbidv 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠) ↔ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)))
161160rabbidv 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
162161, 21eqtr4di 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} = 𝐵)
163 eqeq12 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} ∧ 𝑤 = 𝐵) → (𝑦 = 𝑤 ↔ {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} = 𝐵))
164162, 163syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → ((𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
165164exp4b 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2nd𝑢) = (2nd𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))
166154, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑢) ∧ ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠)) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))
167166ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑢) → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤)))))
168153, 167syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((1st𝑢) = (1st𝑠) → (((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢) → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))))
169168com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1st𝑢) = (1st𝑠) → (𝑖 = 𝑗 → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → (((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))))
170169impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → (((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤)))))
171170com13 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢) → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤)))))
17259, 152, 171syl56 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))))
173172com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))))
174146, 149, 1733syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))))
175174imp 410 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤)))))
176175adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤)))))
177176imp 410 . . . . . . . . . . . . . . . . . . . . . . 23 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))
178177adantld 494 . . . . . . . . . . . . . . . . . . . . . 22 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠))) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))
179178ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st𝑢)) → ((2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠))) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))
180145, 179sylbid 243 . . . . . . . . . . . . . . . . . . . 20 (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st𝑢)) → (𝑥 = ∀𝑔𝑗(1st𝑠) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} → (𝑤 = 𝐵𝑦 = 𝑤))))
181180impd 414 . . . . . . . . . . . . . . . . . . 19 (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st𝑢)) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → (𝑤 = 𝐵𝑦 = 𝑤)))
182181ex 416 . . . . . . . . . . . . . . . . . 18 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) → (𝑥 = ∀𝑔𝑖(1st𝑢) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → (𝑤 = 𝐵𝑦 = 𝑤))))
183182com34 91 . . . . . . . . . . . . . . . . 17 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) → (𝑥 = ∀𝑔𝑖(1st𝑢) → (𝑤 = 𝐵 → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤))))
184183impd 414 . . . . . . . . . . . . . . . 16 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
185184rexlimdva 3276 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
186135, 185jaod 856 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
187186rexlimdva 3276 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
188133a1i 11 . . . . . . . . . . . . . . 15 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
189188rexlimdva 3276 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
190189rexlimdva 3276 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
191187, 190jaod 856 . . . . . . . . . . . 12 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
192191com23 86 . . . . . . . . . . 11 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
193192rexlimdva 3276 . . . . . . . . . 10 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
194115, 193jaod 856 . . . . . . . . 9 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
195194rexlimdva 3276 . . . . . . . 8 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
196 simplll 774 . . . . . . . . . . . . . . . . . . . 20 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → Fun (𝑆‘suc 𝑁))
197 ssel 3946 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆𝑁) → 𝑠 ∈ (𝑆‘suc 𝑁)))
198197adantrd 495 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → ((𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁)))
199198adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ((𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁)))
200199imp 410 . . . . . . . . . . . . . . . . . . . . . 22 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑠 ∈ (𝑆‘suc 𝑁))
201 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑟 ∈ (𝑆‘suc 𝑁))
202201ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑟 ∈ (𝑆‘suc 𝑁))
203200, 202jca 515 . . . . . . . . . . . . . . . . . . . . 21 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
204203adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
20559anim1i 617 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
206205adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
207196, 204, 2063jca 1125 . . . . . . . . . . . . . . . . . . 19 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
208207adantr 484 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
209 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
21066ad2antll 728 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
211208, 209, 210, 67syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤)
212211exp32 424 . . . . . . . . . . . . . . . 16 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
213212impancom 455 . . . . . . . . . . . . . . 15 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
214213expdimp 456 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (𝑣 ∈ (𝑆‘suc 𝑁) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
215214rexlimdv 3275 . . . . . . . . . . . . 13 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))
21690adantrd 495 . . . . . . . . . . . . . . . 16 (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
217216adantr 484 . . . . . . . . . . . . . . 15 ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
218217ad3antlr 730 . . . . . . . . . . . . . 14 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
219218rexlimdva 3276 . . . . . . . . . . . . 13 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
220215, 219jaod 856 . . . . . . . . . . . 12 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤))
221220rexlimdva 3276 . . . . . . . . . . 11 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤))
222 simplll 774 . . . . . . . . . . . . . . . 16 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → Fun (𝑆‘suc 𝑁))
223203adantr 484 . . . . . . . . . . . . . . . 16 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
224100adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
225224adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑢 ∈ (𝑆𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
226225com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑆𝑁) → (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁)))
227226adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁)))
228227impcom 411 . . . . . . . . . . . . . . . . 17 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁))
229105ad2antll 728 . . . . . . . . . . . . . . . . 17 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁))
230228, 229jca 515 . . . . . . . . . . . . . . . 16 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
231222, 223, 2303jca 1125 . . . . . . . . . . . . . . 15 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
232231, 63, 66, 67syl3an 1157 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
2332323exp 1116 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
234233impancom 455 . . . . . . . . . . . 12 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → ((𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
235234rexlimdvv 3285 . . . . . . . . . . 11 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))
236221, 235jaod 856 . . . . . . . . . 10 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))
237236ex 416 . . . . . . . . 9 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
238237rexlimdvva 3286 . . . . . . . 8 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ (𝑆𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
239195, 238jaod 856 . . . . . . 7 ((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𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
24053, 239syl5bi 245 . . . . . 6 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
241240impd 414 . . . . 5 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
242241alrimivv 1930 . . . 4 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑦𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
243 eqeq1 2828 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑦 = 𝐴𝑤 = 𝐴))
244243anbi2d 631 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)))
245244rexbidv 3289 . . . . . . . 8 (𝑦 = 𝑤 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)))
246 eqeq1 2828 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑦 = 𝐵𝑤 = 𝐵))
247246anbi2d 631 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)))
248247rexbidv 3289 . . . . . . . 8 (𝑦 = 𝑤 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)))
249245, 248orbi12d 916 . . . . . . 7 (𝑦 = 𝑤 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵))))
250249rexbidv 3289 . . . . . 6 (𝑦 = 𝑤 → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵))))
2512442rexbidv 3292 . . . . . 6 (𝑦 = 𝑤 → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)))
252250, 251orbi12d 916 . . . . 5 (𝑦 = 𝑤 → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))))
253252mo4 2651 . . . 4 (∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ ∀𝑦𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
254242, 253sylibr 237 . . 3 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
255254alrimiv 1929 . 2 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
256 funopab 6380 . 2 (Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))} ↔ ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
257255, 256sylibr 237 1 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084  wal 1536   = wceq 1538  wcel 2115  ∃*wmo 2622  wne 3014  wral 3133  wrex 3134  {crab 3137  Vcvv 3480  cdif 3916  cun 3917  cin 3918  wss 3919  {csn 4550  cop 4556  {copab 5115  cres 5545  suc csuc 6182  Fun wfun 6339  cfv 6345  (class class class)co 7151  ωcom 7576  1st c1st 7684  2nd c2nd 7685  1oc1o 8093  2oc2o 8094  m cmap 8404  𝑔cgna 32666  𝑔cgol 32667   Sat csat 32668
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fv 6353  df-ov 7154  df-om 7577  df-1st 7686  df-2nd 7687  df-1o 8100  df-2o 8101  df-gona 32673  df-goal 32674
This theorem is referenced by:  satffunlem2  32740
  Copyright terms: Public domain W3C validator