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 34845
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 7874 . . 3 (𝑁 ∈ ω → suc 𝑁 ∈ ω)
2 satfvsucsuc.s . . . 4 𝑆 = (𝑀 Sat 𝐸)
32satfvsuc 34841 . . 3 ((𝑀𝑉𝐸𝑊 ∧ suc 𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
41, 3syl3an3 1162 . 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 2737 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
98anbi2i 622 . . . . . . . . . . . . . . 15 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
109rexbii 3086 . . . . . . . . . . . . . 14 (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
11 satfvsucsuc.b . . . . . . . . . . . . . . . . 17 𝐵 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
1211eqeq2i 2737 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
1312anbi2i 622 . . . . . . . . . . . . . . 15 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
1413rexbii 3086 . . . . . . . . . . . . . 14 (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
1510, 14orbi12i 911 . . . . . . . . . . . . 13 ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
1615rexbii 3086 . . . . . . . . . . . 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 1145 . . . . . . . . . . . . . . . . 17 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑀𝑉𝐸𝑊))
191ancri 549 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
20193ad2ant3 1132 . . . . . . . . . . . . . . . . 17 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
2118, 20jca 511 . . . . . . . . . . . . . . . 16 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
22 sssucid 6434 . . . . . . . . . . . . . . . . 17 𝑁 ⊆ suc 𝑁
2322a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → 𝑁 ⊆ suc 𝑁)
242satfsschain 34844 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁)))
2524imp 406 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
2621, 23, 25syl2an2r 682 . . . . . . . . . . . . . . 15 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
27 undif 4473 . . . . . . . . . . . . . . 15 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) ↔ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
2826, 27sylib 217 . . . . . . . . . . . . . 14 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
2928eqcomd 2730 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))))
3029rexeqdv 3318 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
31 rexun 4182 . . . . . . . . . . . 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, 32bitrid 283 . . . . . . . . . 10 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
34 r19.43 3114 . . . . . . . . . . . . 13 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
3522a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → 𝑁 ⊆ suc 𝑁)
3621, 35jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (((𝑀𝑉𝐸𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁))
3736, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
3837adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆𝑁) ⊆ (𝑆‘suc 𝑁))
3938, 27sylib 217 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))) = (𝑆‘suc 𝑁))
4039eqcomd 2730 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))))
4140rexeqdv 3318 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
42 rexun 4182 . . . . . . . . . . . . . . . . 17 (∃𝑣 ∈ ((𝑆𝑁) ∪ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
4341, 42bitrdi 287 . . . . . . . . . . . . . . . 16 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
4443rexbidv 3170 . . . . . . . . . . . . . . 15 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
4544orbi1d 913 . . . . . . . . . . . . . 14 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
46 r19.43 3114 . . . . . . . . . . . . . . . 16 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
4746orbi1i 910 . . . . . . . . . . . . . . 15 ((∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
48 or32 922 . . . . . . . . . . . . . . . 16 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
49 r19.43 3114 . . . . . . . . . . . . . . . . . 18 (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
5049bicomi 223 . . . . . . . . . . . . . . . . 17 ((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
5150orbi1i 910 . . . . . . . . . . . . . . . 16 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5248, 51bitri 275 . . . . . . . . . . . . . . 15 (((∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
5347, 52bitri 275 . . . . . . . . . . . . . 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, 54bitrid 283 . . . . . . . . . . . 12 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
56 animorr 975 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))))
572satfvsuc 34841 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑆‘suc 𝑁) = ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
5857eleq2d 2811 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ 𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
5958adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ 𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
60 eleq1 2813 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑥, 𝑦⟩ → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
6160adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
62 elun 4140 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑥, 𝑦⟩ ∈ ((𝑆𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
63 opabidw 5514 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))} ↔ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
6463orbi2i 909 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
6562, 64bitri 275 . . . . . . . . . . . . . . . . . . . 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 279 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
687eqcomi 2733 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) = 𝐴
6968eqeq2i 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) ↔ 𝑦 = 𝐴)
7069anbi2i 622 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ↔ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))
7170rexbii 3086 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ↔ ∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))
7211eqcomi 2733 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} = 𝐵
7372eqeq2i 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)} ↔ 𝑦 = 𝐵)
7473anbi2i 622 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))
7574rexbii 3086 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))
7671, 75orbi12i 911 . . . . . . . . . . . . . . . . . . . . 21 ((∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))
7776rexbii 3086 . . . . . . . . . . . . . . . . . . . 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 912 . . . . . . . . . . . . . . . . . 18 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → ((⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8067, 79bitrd 279 . . . . . . . . . . . . . . . . 17 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8180adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑆𝑁) ∨ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)))))
8256, 81mpbird 257 . . . . . . . . . . . . . . 15 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → 𝑠 ∈ (𝑆‘suc 𝑁))
8382orcd 870 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
8483ex 412 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) → (∃𝑢 ∈ (𝑆𝑁)(∃𝑣 ∈ (𝑆𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
85 simplr 766 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → 𝑠 = ⟨𝑥, 𝑦⟩)
86 animorr 975 . . . . . . . . . . . . . . . 16 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
8785, 86jca 511 . . . . . . . . . . . . . . 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 412 . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . 14 ((((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ 𝑠 = ⟨𝑥, 𝑦⟩) ∧ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
9592, 94jca 511 . . . . . . . . . . . . 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 412 . . . . . . . . . . 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 453 . . . . . . . 8 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
1011002eximdv 1914 . . . . . . 7 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))) → ∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))))
102 19.45v 1989 . . . . . . . . 9 (∃𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
103102exbii 1842 . . . . . . . 8 (∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ ∃𝑥(𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
104 19.45v 1989 . . . . . . . 8 (∃𝑥(𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
105103, 104bitri 275 . . . . . . 7 (∃𝑥𝑦(𝑠 ∈ (𝑆‘suc 𝑁) ∨ (𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
106101, 105imbitrdi 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 4123 . . . . . . . . . . . 12 ((𝑆‘suc 𝑁) ∖ (𝑆𝑁)) ⊆ (𝑆‘suc 𝑁)
109 ssrexv 4043 . . . . . . . . . . . 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, 16imbitrdi 250 . . . . . . . . 9 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
113 ssrexv 4043 . . . . . . . . . . . . . . . 16 ((𝑆𝑁) ⊆ (𝑆‘suc 𝑁) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
11437, 113syl 17 . . . . . . . . . . . . . . 15 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))
11592rexbii 3121 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
116114, 115imbitrdi 250 . . . . . . . . . . . . . 14 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))))
117116imp 406 . . . . . . . . . . . . 13 (((𝑀𝑉𝐸𝑊𝑁 ∈ ω) ∧ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)) → ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
118 ssrexv 4043 . . . . . . . . . . . . . . 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 3076 . . . . . . . . . . . . 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 412 . . . . . . . . . 10 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) → (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
124 r19.43 3114 . . . . . . . . . 10 (∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})) ↔ (∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑢 ∈ (𝑆‘suc 𝑁)∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))
125123, 124imbitrrdi 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 611 . . . . . . 7 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))) → (𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
1281272eximdv 1914 . . . . . 6 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → (∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))) → ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})))))
129128orim2d 963 . . . . 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 4140 . . . . 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 5517 . . . . . 6 (𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))} ↔ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))))
133132orbi2i 909 . . . . 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 275 . . . 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 4140 . . . . 5 (𝑠 ∈ ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
136 elopab 5517 . . . . . 6 (𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))} ↔ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))))
137136orbi2i 909 . . . . 5 ((𝑠 ∈ (𝑆‘suc 𝑁) ∨ 𝑠 ∈ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}) ↔ (𝑠 ∈ (𝑆‘suc 𝑁) ∨ ∃𝑥𝑦(𝑠 = ⟨𝑥, 𝑦⟩ ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴)))))
138135, 137bitri 275 . . . 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 2722 . 2 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘suc 𝑁)(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆𝑁))(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = 𝐴))}))
1414, 140eqtrd 2764 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 395  wo 844  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wral 3053  wrex 3062  {crab 3424  cdif 3937  cun 3938  cin 3939  wss 3940  {csn 4620  cop 4626  {copab 5200  cres 5668  suc csuc 6356  cfv 6533  (class class class)co 7401  ωcom 7848  1st c1st 7966  2nd c2nd 7967  m cmap 8816  𝑔cgna 34814  𝑔cgol 34815   Sat csat 34816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-sat 34823
This theorem is referenced by:  satffunlem2  34888
  Copyright terms: Public domain W3C validator