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 33327
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 7737 . . 3 (𝑁 ∈ ω → suc 𝑁 ∈ ω)
2 satfvsucsuc.s . . . 4 𝑆 = (𝑀 Sat 𝐸)
32satfvsuc 33323 . . 3 ((𝑀𝑉𝐸𝑊 ∧ suc 𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
41, 3syl3an3 1164 . 2 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
5 orc 864 . . . . . . 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 2751 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
98anbi2i 623 . . . . . . . . . . . . . . 15 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
109rexbii 3181 . . . . . . . . . . . . . 14 (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
11 satfvsucsuc.b . . . . . . . . . . . . . . . . 17 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
1211eqeq2i 2751 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
1312anbi2i 623 . . . . . . . . . . . . . . 15 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
1413rexbii 3181 . . . . . . . . . . . . . 14 (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
1510, 14orbi12i 912 . . . . . . . . . . . . 13 ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
1615rexbii 3181 . . . . . . . . . . . 12 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
1716bicomi 223 . . . . . . . . . . 11 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
18 3simpa 1147 . . . . . . . . . . . . . . . . 17 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑀𝑉𝐸𝑊))
191ancri 550 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
20193ad2ant3 1134 . . . . . . . . . . . . . . . . 17 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
2118, 20jca 512 . . . . . . . . . . . . . . . 16 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
22 sssucid 6343 . . . . . . . . . . . . . . . . 17 𝑁 ⊆ suc 𝑁
2322a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → 𝑁 ⊆ suc 𝑁)
242satfsschain 33326 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)))
2524imp 407 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
2621, 23, 25syl2an2r 682 . . . . . . . . . . . . . . 15 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
27 undif 4415 . . . . . . . . . . . . . . 15 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) ↔ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
2826, 27sylib 217 . . . . . . . . . . . . . 14 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
2928eqcomd 2744 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))))
3029rexeqdv 3349 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
31 rexun 4124 . . . . . . . . . . . 12 (∃𝑢 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
3230, 31bitrdi 287 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
3317, 32syl5bb 283 . . . . . . . . . 10 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
34 r19.43 3280 . . . . . . . . . . . . 13 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
3522a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → 𝑁 ⊆ suc 𝑁)
3621, 35jca 512 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁))
3736, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
3837adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
3938, 27sylib 217 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
4039eqcomd 2744 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))))
4140rexeqdv 3349 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
42 rexun 4124 . . . . . . . . . . . . . . . . 17 (∃𝑣 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
4341, 42bitrdi 287 . . . . . . . . . . . . . . . 16 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
4443rexbidv 3226 . . . . . . . . . . . . . . 15 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
4544orbi1d 914 . . . . . . . . . . . . . 14 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
46 r19.43 3280 . . . . . . . . . . . . . . . 16 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
4746orbi1i 911 . . . . . . . . . . . . . . 15 ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
48 or32 923 . . . . . . . . . . . . . . . 16 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
49 r19.43 3280 . . . . . . . . . . . . . . . . . 18 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
5049bicomi 223 . . . . . . . . . . . . . . . . 17 ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
5150orbi1i 911 . . . . . . . . . . . . . . . 16 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5248, 51bitri 274 . . . . . . . . . . . . . . 15 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5347, 52bitri 274 . . . . . . . . . . . . . 14 ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5445, 53bitrdi 287 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
5534, 54syl5bb 283 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
56 animorr 976 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
572satfvsuc 33323 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
5857eleq2d 2824 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ 𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
5958adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ 𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
60 eleq1 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑥, 𝑦⟩ → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
6160adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
62 elun 4083 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
63 opabidw 5437 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))} ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
6463orbi2i 910 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
6562, 64bitri 274 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
6661, 65bitrdi 287 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
6759, 66bitrd 278 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
687eqcomi 2747 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = 𝐴
6968eqeq2i 2751 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) ↔ 𝑦 = 𝐴)
7069anbi2i 623 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))
7170rexbii 3181 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ↔ ∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))
7211eqcomi 2747 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} = 𝐵
7372eqeq2i 2751 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} ↔ 𝑦 = 𝐵)
7473anbi2i 623 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))
7574rexbii 3181 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))
7671, 75orbi12i 912 . . . . . . . . . . . . . . . . . . . . 21 ((∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
7776rexbii 3181 . . . . . . . . . . . . . . . . . . . 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 913 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8067, 79bitrd 278 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8180adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8256, 81mpbird 256 . . . . . . . . . . . . . . 15 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → 𝑠 ∈ (𝑆‘suc 𝑁))
8382orcd 870 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
8483ex 413 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
85 simplr 766 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → 𝑠 = ⟨𝑥, 𝑦⟩)
86 animorr 976 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
8785, 86jca 512 . . . . . . . . . . . . . . 15 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
8887olcd 871 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
8988ex 413 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9084, 89jaod 856 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9155, 90sylbid 239 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
92 simplr 766 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → 𝑠 = ⟨𝑥, 𝑦⟩)
93 orc 864 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
9493adantl 482 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
9592, 94jca 512 . . . . . . . . . . . . 13 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
9695olcd 871 . . . . . . . . . . . 12 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
9796ex 413 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9891, 97jaod 856 . . . . . . . . . 10 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
9933, 98sylbid 239 . . . . . . . . 9 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
10099expimpd 454 . . . . . . . 8 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
1011002eximdv 1922 . . . . . . 7 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → ∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
102 19.45v 1997 . . . . . . . . 9 (∃𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
103102exbii 1850 . . . . . . . 8 (∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ ∃𝑥(𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
104 19.45v 1997 . . . . . . . 8 (∃𝑥(𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
105103, 104bitri 274 . . . . . . 7 (∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
106101, 105syl6ib 250 . . . . . 6 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
1076, 106jaod 856 . . . . 5 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
108 difss 4066 . . . . . . . . . . . 12 ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ⊆ (𝑆‘suc 𝑁)
109 ssrexv 3988 . . . . . . . . . . . 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 250 . . . . . . . . 9 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
113 ssrexv 3988 . . . . . . . . . . . . . . . 16 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
11437, 113syl 17 . . . . . . . . . . . . . . 15 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
11592rexbii 3182 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
116114, 115syl6ib 250 . . . . . . . . . . . . . 14 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))))
117116imp 407 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
118 ssrexv 3988 . . . . . . . . . . . . . . 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 3178 . . . . . . . . . . . . 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 870 . . . . . . . . . . 11 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
123122ex 413 . . . . . . . . . 10 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
124 r19.43 3280 . . . . . . . . . 10 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
125123, 124syl6ibr 251 . . . . . . . . 9 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
126112, 125jaod 856 . . . . . . . 8 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
127126anim2d 612 . . . . . . 7 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
1281272eximdv 1922 . . . . . 6 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))) → ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
129128orim2d 964 . . . . 5 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))))
130107, 129impbid 211 . . . 4 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
131 elun 4083 . . . . 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 5440 . . . . . 6 (𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))} ↔ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
133132orbi2i 910 . . . . 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 274 . . . 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 4083 . . . . 5 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
136 elopab 5440 . . . . . 6 (𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))} ↔ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
137136orbi2i 910 . . . . 5 ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
138135, 137bitri 274 . . . 4 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
139130, 134, 1383bitr4g 314 . . 3 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ 𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))})))
140139eqrdv 2736 . 2 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
1414, 140eqtrd 2778 1 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wex 1782  wcel 2106  wral 3064  wrex 3065  {crab 3068  cdif 3884  cun 3885  cin 3886  wss 3887  {csn 4561  cop 4567  {copab 5136  cres 5591  suc csuc 6268  cfv 6433  (class class class)co 7275  ωcom 7712  1st c1st 7829  2nd c2nd 7830  m cmap 8615  𝑔cgna 33296  𝑔cgol 33297   Sat csat 33298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-sat 33305
This theorem is referenced by:  satffunlem2  33370
  Copyright terms: Public domain W3C validator