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 33102
Description: Lemma 1 for satffunlem2 33106. (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 6739 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → (1st𝑢) = (1st𝑠))
3 simpr 488 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑣 = 𝑟) → 𝑣 = 𝑟)
43fveq2d 6739 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → (1st𝑣) = (1st𝑟))
52, 4oveq12d 7249 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑣 = 𝑟) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
65eqeq2d 2749 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))))
7 satffunlem2lem1.a . . . . . . . . . . . . . 14 𝐴 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
81fveq2d 6739 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑠𝑣 = 𝑟) → (2nd𝑢) = (2nd𝑠))
93fveq2d 6739 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑠𝑣 = 𝑟) → (2nd𝑣) = (2nd𝑟))
108, 9ineq12d 4142 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑣 = 𝑟) → ((2nd𝑢) ∩ (2nd𝑣)) = ((2nd𝑠) ∩ (2nd𝑟)))
1110difeq2d 4051 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))
127, 11syl5eq 2791 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑣 = 𝑟) → 𝐴 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))
1312eqeq2d 2749 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
146, 13anbi12d 634 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
1514cbvrexdva 3382 . . . . . . . . . 10 (𝑢 = 𝑠 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
16 simpr 488 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑖 = 𝑗) → 𝑖 = 𝑗)
17 fveq2 6735 . . . . . . . . . . . . . . 15 (𝑢 = 𝑠 → (1st𝑢) = (1st𝑠))
1817adantr 484 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑖 = 𝑗) → (1st𝑢) = (1st𝑠))
1916, 18goaleq12d 33049 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑖 = 𝑗) → ∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠))
2019eqeq2d 2749 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑖 = 𝑗) → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ 𝑥 = ∀𝑔𝑗(1st𝑠)))
21 satffunlem2lem1.b . . . . . . . . . . . . . 14 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
2221eqeq2i 2751 . . . . . . . . . . . . 13 (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
23 opeq1 4798 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → ⟨𝑖, 𝑧⟩ = ⟨𝑗, 𝑧⟩)
2423sneqd 4567 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → {⟨𝑖, 𝑧⟩} = {⟨𝑗, 𝑧⟩})
25 sneq 4565 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑗 → {𝑖} = {𝑗})
2625difeq2d 4051 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (ω ∖ {𝑖}) = (ω ∖ {𝑗}))
2726reseq2d 5865 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑎 ↾ (ω ∖ {𝑖})) = (𝑎 ↾ (ω ∖ {𝑗})))
2824, 27uneq12d 4092 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))))
2928adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑢 = 𝑠𝑖 = 𝑗) → ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))))
30 fveq2 6735 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑠 → (2nd𝑢) = (2nd𝑠))
3130adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑢 = 𝑠𝑖 = 𝑗) → (2nd𝑢) = (2nd𝑠))
3229, 31eleq12d 2833 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑠𝑖 = 𝑗) → (({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢) ↔ ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)))
3332ralbidv 3119 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑠𝑖 = 𝑗) → (∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢) ↔ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)))
3433rabbidv 3402 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑖 = 𝑗) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})
3534eqeq2d 2749 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑖 = 𝑗) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}))
3622, 35syl5bb 286 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑖 = 𝑗) → (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}))
3720, 36anbi12d 634 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑖 = 𝑗) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})))
3837cbvrexdva 3382 . . . . . . . . . 10 (𝑢 = 𝑠 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})))
3915, 38orbi12d 919 . . . . . . . . 9 (𝑢 = 𝑠 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}))))
4039cbvrexvw 3371 . . . . . . . 8 (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})))
41 fveq2 6735 . . . . . . . . . . . . 13 (𝑣 = 𝑟 → (1st𝑣) = (1st𝑟))
4217, 41oveqan12d 7250 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
4342eqeq2d 2749 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))))
447eqeq2i 2751 . . . . . . . . . . . 12 (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
45 fveq2 6735 . . . . . . . . . . . . . . 15 (𝑣 = 𝑟 → (2nd𝑣) = (2nd𝑟))
4630, 45ineqan12d 4143 . . . . . . . . . . . . . 14 ((𝑢 = 𝑠𝑣 = 𝑟) → ((2nd𝑢) ∩ (2nd𝑣)) = ((2nd𝑠) ∩ (2nd𝑟)))
4746difeq2d 4051 . . . . . . . . . . . . 13 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))
4847eqeq2d 2749 . . . . . . . . . . . 12 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) ↔ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
4944, 48syl5bb 286 . . . . . . . . . . 11 ((𝑢 = 𝑠𝑣 = 𝑟) → (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
5043, 49anbi12d 634 . . . . . . . . . 10 ((𝑢 = 𝑠𝑣 = 𝑟) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
5150cbvrexdva 3382 . . . . . . . . 9 (𝑢 = 𝑠 → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))))
5251cbvrexvw 3371 . . . . . . . 8 (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑠 ∈ (𝑆𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
5340, 52orbi12i 915 . . . . . . 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 785 . . . . . . . . . . . . . . . . . . . 20 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → Fun (𝑆‘suc 𝑁))
55 eldifi 4055 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁))
5655adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁))
5756anim1i 618 . . . . . . . . . . . . . . . . . . . . 21 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
5857ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
59 eldifi 4055 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁))
6059adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → 𝑢 ∈ (𝑆‘suc 𝑁))
6160anim1i 618 . . . . . . . . . . . . . . . . . . . 20 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
6254, 58, 613jca 1130 . . . . . . . . . . . . . . . . . . 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 2751 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝐴𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
6564biimpi 219 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝐴𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
6665anim2i 620 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
67 satffunlem 33099 . . . . . . . . . . . . . . . . . . 19 (((Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)
6862, 63, 66, 67syl3an 1162 . . . . . . . . . . . . . . . . . 18 (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
69683exp 1121 . . . . . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
72 eqeq1 2742 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ ((1st𝑠)⊼𝑔(1st𝑟)) = ∀𝑔𝑖(1st𝑢)))
73 fvex 6748 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑠) ∈ V
74 fvex 6748 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑟) ∈ V
75 gonafv 33048 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑠) ∈ V ∧ (1st𝑟) ∈ V) → ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
7673, 74, 75mp2an 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩
77 df-goal 33040 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔𝑖(1st𝑢) = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩
7876, 77eqeq12i 2756 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑠)⊼𝑔(1st𝑟)) = ∀𝑔𝑖(1st𝑢) ↔ ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩)
79 1oex 8235 . . . . . . . . . . . . . . . . . . . . . . . 24 1o ∈ V
80 opex 5362 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨(1st𝑠), (1st𝑟)⟩ ∈ V
8179, 80opth 5374 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ = ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ ↔ (1o = 2o ∧ ⟨(1st𝑠), (1st𝑟)⟩ = ⟨𝑖, (1st𝑢)⟩))
82 1one2o 8391 . . . . . . . . . . . . . . . . . . . . . . . . 25 1o ≠ 2o
83 df-ne 2942 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
9671, 95jaod 859 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
9796rexlimdva 3211 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
98 simp-4l 783 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → Fun (𝑆‘suc 𝑁))
9957adantr 484 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
100 ssel 3907 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
101100ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . 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 4055 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑣 ∈ (𝑆‘suc 𝑁))
106105ad2antll 729 . . . . . . . . . . . . . . . . . . 19 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁))
107104, 106jca 515 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
10898, 99, 1073jca 1130 . . . . . . . . . . . . . . . . 17 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
109108, 63, 66, 67syl3an 1162 . . . . . . . . . . . . . . . 16 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
1101093exp 1121 . . . . . . . . . . . . . . 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 3221 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → 𝑦 = 𝑤)))
11397, 112jaod 859 . . . . . . . . . . . 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 3211 . . . . . . . . . 10 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
116 eqeq1 2742 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ∀𝑔𝑗(1st𝑠) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ∀𝑔𝑗(1st𝑠) = ((1st𝑢)⊼𝑔(1st𝑣))))
117 df-goal 33040 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔𝑗(1st𝑠) = ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩
118 fvex 6748 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑢) ∈ V
119 fvex 6748 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑣) ∈ V
120 gonafv 33048 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑢) ∈ V ∧ (1st𝑣) ∈ V) → ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
121118, 119, 120mp2an 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩
122117, 121eqeq12i 2756 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑔𝑗(1st𝑠) = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
123 2oex 8239 . . . . . . . . . . . . . . . . . . . . . . . 24 2o ∈ V
124 opex 5362 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗, (1st𝑠)⟩ ∈ V
125123, 124opth 5374 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ ↔ (2o = 1o ∧ ⟨𝑗, (1st𝑠)⟩ = ⟨(1st𝑢), (1st𝑣)⟩))
12686eqcoms 2746 . . . . . . . . . . . . . . . . . . . . . . . 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 3209 . . . . . . . . . . . . . . . 16 (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤))
135134a1i 11 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
136 eqeq1 2742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ∀𝑔𝑖(1st𝑢) → (𝑥 = ∀𝑔𝑗(1st𝑠) ↔ ∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠)))
13777, 117eqeq12i 2756 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠) ↔ ⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ = ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩)
138 opex 5362 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖, (1st𝑢)⟩ ∈ V
139123, 138opth 5374 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨2o, ⟨𝑖, (1st𝑢)⟩⟩ = ⟨2o, ⟨𝑗, (1st𝑠)⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, (1st𝑢)⟩ = ⟨𝑗, (1st𝑠)⟩))
140 vex 3424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑖 ∈ V
141140, 118opth 5374 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑖, (1st𝑢)⟩ = ⟨𝑗, (1st𝑠)⟩ ↔ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠)))
142141anbi2i 626 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2o = 2o ∧ ⟨𝑖, (1st𝑢)⟩ = ⟨𝑗, (1st𝑠)⟩) ↔ (2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠))))
143137, 139, 1423bitri 300 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑔𝑖(1st𝑢) = ∀𝑔𝑗(1st𝑠) ↔ (2o = 2o ∧ (𝑖 = 𝑗 ∧ (1st𝑢) = (1st𝑠))))
144136, 143bitrdi 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 7835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st𝑢) = (1st𝑠) → (((𝑆‘suc 𝑁)‘(1st𝑢)) = (2nd𝑢) ↔ ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑢)))
154 eqtr2 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑢) ∧ ((𝑆‘suc 𝑁)‘(1st𝑠)) = (2nd𝑠)) → (2nd𝑢) = (2nd𝑠))
15528eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑖 = 𝑗 → ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))))
156155adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))))
157 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (2nd𝑢) = (2nd𝑠))
158157eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (2nd𝑠) = (2nd𝑢))
159156, 158eleq12d 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠) ↔ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)))
160159ralbidv 3119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → (∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠) ↔ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)))
161160rabbidv 3402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
162161, 21eqtr4di 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((2nd𝑢) = (2nd𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)} = 𝐵)
163 eqeq12 2755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . . 15 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
186135, 185jaod 859 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
187186rexlimdva 3211 . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
190189rexlimdva 3211 . . . . . . . . . . . . 13 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → 𝑦 = 𝑤)))
191187, 190jaod 859 . . . . . . . . . . . 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 3211 . . . . . . . . . 10 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
194115, 193jaod 859 . . . . . . . . 9 (((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
195194rexlimdva 3211 . . . . . . . 8 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
196 simplll 775 . . . . . . . . . . . . . . . . . . . 20 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → Fun (𝑆‘suc 𝑁))
197 ssel 3907 . . . . . . . . . . . . . . . . . . . . . . . . 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 4055 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) → 𝑟 ∈ (𝑆‘suc 𝑁))
202201ad2antll 729 . . . . . . . . . . . . . . . . . . . . . 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 618 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
206205adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
207196, 204, 2063jca 1130 . . . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))))
21066ad2antll 729 . . . . . . . . . . . . . . . . . 18 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
211208, 209, 210, 67syl3anc 1373 . . . . . . . . . . . . . . . . 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 3210 . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . 14 ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
219218rexlimdva 3211 . . . . . . . . . . . . 13 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
220215, 219jaod 859 . . . . . . . . . . . 12 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤))
221220rexlimdva 3211 . . . . . . . . . . 11 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤))
222 simplll 775 . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . 17 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁))
230228, 229jca 515 . . . . . . . . . . . . . . . 16 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
231222, 223, 2303jca 1130 . . . . . . . . . . . . . . 15 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
232231, 63, 66, 67syl3an 1162 . . . . . . . . . . . . . 14 (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑢 ∈ (𝑆𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
2332323exp 1121 . . . . . . . . . . . . 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 3220 . . . . . . . . . . 11 ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))))) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))
236221, 235jaod 859 . . . . . . . . . 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 3221 . . . . . . . 8 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ (𝑆𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
239195, 238jaod 859 . . . . . . 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 1936 . . . 4 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑦𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
243 eqeq1 2742 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑦 = 𝐴𝑤 = 𝐴))
244243anbi2d 632 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)))
245244rexbidv 3224 . . . . . . . 8 (𝑦 = 𝑤 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)))
246 eqeq1 2742 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑦 = 𝐵𝑤 = 𝐵))
247246anbi2d 632 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)))
248247rexbidv 3224 . . . . . . . 8 (𝑦 = 𝑤 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)))
249245, 248orbi12d 919 . . . . . . 7 (𝑦 = 𝑤 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵))))
250249rexbidv 3224 . . . . . 6 (𝑦 = 𝑤 → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵))))
2512442rexbidv 3227 . . . . . 6 (𝑦 = 𝑤 → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴)))
252250, 251orbi12d 919 . . . . 5 (𝑦 = 𝑤 → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = 𝐴))))
253252mo4 2566 . . . 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 1935 . 2 ((Fun (𝑆‘suc 𝑁) ∧ (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
256 funopab 6432 . 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 847  w3a 1089  wal 1541   = wceq 1543  wcel 2111  ∃*wmo 2538  wne 2941  wral 3062  wrex 3063  {crab 3066  Vcvv 3420  cdif 3877  cun 3878  cin 3879  wss 3880  {csn 4555  cop 4561  {copab 5129  cres 5567  suc csuc 6232  Fun wfun 6391  cfv 6397  (class class class)co 7231  ωcom 7662  1st c1st 7777  2nd c2nd 7778  1oc1o 8215  2oc2o 8216  m cmap 8528  𝑔cgna 33032  𝑔cgol 33033   Sat csat 33034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336  ax-un 7541
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fv 6405  df-ov 7234  df-om 7663  df-1st 7779  df-2nd 7780  df-1o 8222  df-2o 8223  df-gona 33039  df-goal 33040
This theorem is referenced by:  satffunlem2  33106
  Copyright terms: Public domain W3C validator