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

Theorem satfvsucsuc 32901
Description: The satisfaction predicate as function over wff codes of height (𝑁 + 1), expressed by the minimally necessary satisfaction predicates as function over wff codes of height 𝑁. (Contributed by AV, 21-Oct-2023.)
Hypotheses
Ref Expression
satfvsucsuc.s 𝑆 = (𝑀 Sat 𝐸)
satfvsucsuc.a 𝐴 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
satfvsucsuc.b 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
Assertion
Ref Expression
satfvsucsuc ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
Distinct variable groups:   𝐸,𝑎,𝑖,𝑢,𝑣,𝑥,𝑦,𝑧   𝑀,𝑎,𝑖,𝑢,𝑣,𝑥,𝑦,𝑧   𝑢,𝑁,𝑣,𝑥,𝑦   𝑢,𝑆,𝑣,𝑦,𝑥   𝑢,𝑉,𝑥,𝑦   𝑢,𝑊,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑣,𝑢,𝑖,𝑎)   𝐵(𝑥,𝑦,𝑧,𝑣,𝑢,𝑖,𝑎)   𝑆(𝑧,𝑖,𝑎)   𝑁(𝑧,𝑖,𝑎)   𝑉(𝑧,𝑣,𝑖,𝑎)   𝑊(𝑧,𝑣,𝑖,𝑎)

Proof of Theorem satfvsucsuc
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 peano2 7624 . . 3 (𝑁 ∈ ω → suc 𝑁 ∈ ω)
2 satfvsucsuc.s . . . 4 𝑆 = (𝑀 Sat 𝐸)
32satfvsuc 32897 . . 3 ((𝑀𝑉𝐸𝑊 ∧ suc 𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
41, 3syl3an3 1166 . 2 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
5 orc 866 . . . . . . 7 (𝑠 ∈ (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
65a1i 11 . . . . . 6 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑠 ∈ (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
7 satfvsucsuc.a . . . . . . . . . . . . . . . . 17 𝐴 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
87eqeq2i 2752 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
98anbi2i 626 . . . . . . . . . . . . . . 15 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
109rexbii 3162 . . . . . . . . . . . . . 14 (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
11 satfvsucsuc.b . . . . . . . . . . . . . . . . 17 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
1211eqeq2i 2752 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
1312anbi2i 626 . . . . . . . . . . . . . . 15 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
1413rexbii 3162 . . . . . . . . . . . . . 14 (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
1510, 14orbi12i 914 . . . . . . . . . . . . 13 ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
1615rexbii 3162 . . . . . . . . . . . 12 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
1716bicomi 227 . . . . . . . . . . 11 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
18 3simpa 1149 . . . . . . . . . . . . . . . . 17 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑀𝑉𝐸𝑊))
191ancri 553 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
20193ad2ant3 1136 . . . . . . . . . . . . . . . . 17 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
2118, 20jca 515 . . . . . . . . . . . . . . . 16 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
22 sssucid 6250 . . . . . . . . . . . . . . . . 17 𝑁 ⊆ suc 𝑁
2322a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → 𝑁 ⊆ suc 𝑁)
242satfsschain 32900 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)))
2524imp 410 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
2621, 23, 25syl2an2r 685 . . . . . . . . . . . . . . 15 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
27 undif 4372 . . . . . . . . . . . . . . 15 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) ↔ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
2826, 27sylib 221 . . . . . . . . . . . . . 14 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
2928eqcomd 2745 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))))
3029rexeqdv 3318 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
31 rexun 4081 . . . . . . . . . . . 12 (∃𝑢 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
3230, 31bitrdi 290 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
3317, 32syl5bb 286 . . . . . . . . . 10 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
34 r19.43 3256 . . . . . . . . . . . . 13 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
3522a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → 𝑁 ⊆ suc 𝑁)
3621, 35jca 515 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁))
3736, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
3837adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
3938, 27sylib 221 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
4039eqcomd 2745 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))))
4140rexeqdv 3318 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
42 rexun 4081 . . . . . . . . . . . . . . . . 17 (∃𝑣 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
4341, 42bitrdi 290 . . . . . . . . . . . . . . . 16 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
4443rexbidv 3208 . . . . . . . . . . . . . . 15 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
4544orbi1d 916 . . . . . . . . . . . . . 14 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
46 r19.43 3256 . . . . . . . . . . . . . . . 16 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
4746orbi1i 913 . . . . . . . . . . . . . . 15 ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
48 or32 925 . . . . . . . . . . . . . . . 16 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
49 r19.43 3256 . . . . . . . . . . . . . . . . . 18 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
5049bicomi 227 . . . . . . . . . . . . . . . . 17 ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
5150orbi1i 913 . . . . . . . . . . . . . . . 16 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5248, 51bitri 278 . . . . . . . . . . . . . . 15 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5347, 52bitri 278 . . . . . . . . . . . . . 14 ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5445, 53bitrdi 290 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
5534, 54syl5bb 286 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
56 animorr 978 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
572satfvsuc 32897 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
5857eleq2d 2819 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ 𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
5958adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ 𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
60 eleq1 2821 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑥, 𝑦⟩ → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
6160adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
62 elun 4040 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
63 opabidw 5381 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))} ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
6463orbi2i 912 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
6562, 64bitri 278 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
6661, 65bitrdi 290 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
6759, 66bitrd 282 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
687eqcomi 2748 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = 𝐴
6968eqeq2i 2752 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) ↔ 𝑦 = 𝐴)
7069anbi2i 626 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))
7170rexbii 3162 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ↔ ∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))
7211eqcomi 2748 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} = 𝐵
7372eqeq2i 2752 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} ↔ 𝑦 = 𝐵)
7473anbi2i 626 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))
7574rexbii 3162 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))
7671, 75orbi12i 914 . . . . . . . . . . . . . . . . . . . . 21 ((∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
7776rexbii 3162 . . . . . . . . . . . . . . . . . . . 20 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
7877a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
7978orbi2d 915 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8067, 79bitrd 282 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8180adantr 484 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8256, 81mpbird 260 . . . . . . . . . . . . . . 15 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → 𝑠 ∈ (𝑆‘suc 𝑁))
8382orcd 872 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
8483ex 416 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
85 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → 𝑠 = ⟨𝑥, 𝑦⟩)
86 animorr 978 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
8785, 86jca 515 . . . . . . . . . . . . . . 15 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
8887olcd 873 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
8988ex 416 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9084, 89jaod 858 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9155, 90sylbid 243 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
92 simplr 769 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → 𝑠 = ⟨𝑥, 𝑦⟩)
93 orc 866 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
9493adantl 485 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
9592, 94jca 515 . . . . . . . . . . . . 13 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
9695olcd 873 . . . . . . . . . . . 12 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
9796ex 416 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9891, 97jaod 858 . . . . . . . . . 10 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9933, 98sylbid 243 . . . . . . . . 9 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
10099expimpd 457 . . . . . . . 8 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
1011002eximdv 1926 . . . . . . 7 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → ∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
102 19.45v 2005 . . . . . . . . 9 (∃𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
103102exbii 1854 . . . . . . . 8 (∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ ∃𝑥(𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
104 19.45v 2005 . . . . . . . 8 (∃𝑥(𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
105103, 104bitri 278 . . . . . . 7 (∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
106101, 105syl6ib 254 . . . . . 6 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
1076, 106jaod 858 . . . . 5 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
108 difss 4023 . . . . . . . . . . . 12 ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ⊆ (𝑆‘suc 𝑁)
109 ssrexv 3945 . . . . . . . . . . . 12 (((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ⊆ (𝑆‘suc 𝑁) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
110108, 109ax-mp 5 . . . . . . . . . . 11 (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
111110a1i 11 . . . . . . . . . 10 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
112111, 16syl6ib 254 . . . . . . . . 9 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
113 ssrexv 3945 . . . . . . . . . . . . . . . 16 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
11437, 113syl 17 . . . . . . . . . . . . . . 15 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
11592rexbii 3163 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
116114, 115syl6ib 254 . . . . . . . . . . . . . 14 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))))
117116imp 410 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
118 ssrexv 3945 . . . . . . . . . . . . . . 15 (((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ⊆ (𝑆‘suc 𝑁) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))))
119108, 118ax-mp 5 . . . . . . . . . . . . . 14 (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
120119reximi 3158 . . . . . . . . . . . . 13 (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
121117, 120syl 17 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
122121orcd 872 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
123122ex 416 . . . . . . . . . 10 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
124 r19.43 3256 . . . . . . . . . 10 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
125123, 124syl6ibr 255 . . . . . . . . 9 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
126112, 125jaod 858 . . . . . . . 8 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
127126anim2d 615 . . . . . . 7 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
1281272eximdv 1926 . . . . . 6 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))) → ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
129128orim2d 966 . . . . 5 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))))
130107, 129impbid 215 . . . 4 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
131 elun 4040 . . . . 5 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
132 elopab 5383 . . . . . 6 (𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))} ↔ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
133132orbi2i 912 . . . . 5 ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
134131, 133bitri 278 . . . 4 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
135 elun 4040 . . . . 5 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
136 elopab 5383 . . . . . 6 (𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))} ↔ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
137136orbi2i 912 . . . . 5 ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
138135, 137bitri 278 . . . 4 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
139130, 134, 1383bitr4g 317 . . 3 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ 𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))})))
140139eqrdv 2737 . 2 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
1414, 140eqtrd 2774 1 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 846  w3a 1088   = wceq 1542  wex 1786  wcel 2114  wral 3054  wrex 3055  {crab 3058  cdif 3841  cun 3842  cin 3843  wss 3844  {csn 4517  cop 4523  {copab 5093  cres 5528  suc csuc 6175  cfv 6340  (class class class)co 7173  ωcom 7602  1st c1st 7715  2nd c2nd 7716  m cmap 8440  𝑔cgna 32870  𝑔cgol 32871   Sat csat 32872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482  ax-inf2 9180
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-ov 7176  df-oprab 7177  df-mpo 7178  df-om 7603  df-wrecs 7979  df-recs 8040  df-rdg 8078  df-sat 32879
This theorem is referenced by:  satffunlem2  32944
  Copyright terms: Public domain W3C validator