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

Theorem satfv1 32496
 Description: The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023.)
Hypothesis
Ref Expression
satfv1.s 𝑆 = (𝑀 Sat 𝐸)
Assertion
Ref Expression
satfv1 ((𝑀𝑉𝐸𝑊) → (𝑆‘1o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))}))
Distinct variable groups:   𝐸,𝑎,𝑖,𝑗,𝑘,𝑙,𝑥,𝑦   𝑛,𝐸,𝑧,𝑎,𝑖,𝑗,𝑥,𝑦   𝑀,𝑎,𝑖,𝑗,𝑘,𝑙,𝑥,𝑦   𝑛,𝑀,𝑧   𝑥,𝑆,𝑦   𝑥,𝑉,𝑦   𝑥,𝑊,𝑦
Allowed substitution hints:   𝑆(𝑧,𝑖,𝑗,𝑘,𝑛,𝑎,𝑙)   𝑉(𝑧,𝑖,𝑗,𝑘,𝑛,𝑎,𝑙)   𝑊(𝑧,𝑖,𝑗,𝑘,𝑛,𝑎,𝑙)

Proof of Theorem satfv1
Dummy variables 𝑏 𝑐 𝑑 𝑒 𝑜 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-1o 8096 . . . 4 1o = suc ∅
21fveq2i 6669 . . 3 (𝑆‘1o) = (𝑆‘suc ∅)
32a1i 11 . 2 ((𝑀𝑉𝐸𝑊) → (𝑆‘1o) = (𝑆‘suc ∅))
4 peano1 7592 . . 3 ∅ ∈ ω
5 satfv1.s . . . 4 𝑆 = (𝑀 Sat 𝐸)
65satfvsuc 32494 . . 3 ((𝑀𝑉𝐸𝑊 ∧ ∅ ∈ ω) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}))}))
74, 6mp3an3 1443 . 2 ((𝑀𝑉𝐸𝑊) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}))}))
85satfv0 32491 . . . . . . 7 ((𝑀𝑉𝐸𝑊) → (𝑆‘∅) = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})})
98rexeqdv 3421 . . . . . 6 ((𝑀𝑉𝐸𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)})) ↔ ∃𝑜 ∈ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}))))
10 eqid 2825 . . . . . . 7 {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})} = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})}
11 vex 3502 . . . . . . . . . . . . 13 𝑒 ∈ V
12 vex 3502 . . . . . . . . . . . . 13 𝑏 ∈ V
1311, 12op1std 7693 . . . . . . . . . . . 12 (𝑜 = ⟨𝑒, 𝑏⟩ → (1st𝑜) = 𝑒)
1413oveq1d 7166 . . . . . . . . . . 11 (𝑜 = ⟨𝑒, 𝑏⟩ → ((1st𝑜)⊼𝑔(1st𝑝)) = (𝑒𝑔(1st𝑝)))
1514eqeq2d 2836 . . . . . . . . . 10 (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ↔ 𝑥 = (𝑒𝑔(1st𝑝))))
1611, 12op2ndd 7694 . . . . . . . . . . . . 13 (𝑜 = ⟨𝑒, 𝑏⟩ → (2nd𝑜) = 𝑏)
1716ineq1d 4191 . . . . . . . . . . . 12 (𝑜 = ⟨𝑒, 𝑏⟩ → ((2nd𝑜) ∩ (2nd𝑝)) = (𝑏 ∩ (2nd𝑝)))
1817difeq2d 4102 . . . . . . . . . . 11 (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝))) = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝))))
1918eqeq2d 2836 . . . . . . . . . 10 (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝))) ↔ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))))
2015, 19anbi12d 630 . . . . . . . . 9 (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ↔ (𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝))))))
2120rexbidv 3301 . . . . . . . 8 (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝))))))
22 eqidd 2826 . . . . . . . . . . . 12 (𝑜 = ⟨𝑒, 𝑏⟩ → 𝑛 = 𝑛)
2322, 13goaleq12d 32484 . . . . . . . . . . 11 (𝑜 = ⟨𝑒, 𝑏⟩ → ∀𝑔𝑛(1st𝑜) = ∀𝑔𝑛𝑒)
2423eqeq2d 2836 . . . . . . . . . 10 (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ∀𝑔𝑛(1st𝑜) ↔ 𝑥 = ∀𝑔𝑛𝑒))
2516eleq2d 2902 . . . . . . . . . . . . 13 (𝑜 = ⟨𝑒, 𝑏⟩ → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜) ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
2625ralbidv 3201 . . . . . . . . . . . 12 (𝑜 = ⟨𝑒, 𝑏⟩ → (∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜) ↔ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
2726rabbidv 3485 . . . . . . . . . . 11 (𝑜 = ⟨𝑒, 𝑏⟩ → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})
2827eqeq2d 2836 . . . . . . . . . 10 (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))
2924, 28anbi12d 630 . . . . . . . . 9 (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}) ↔ (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
3029rexbidv 3301 . . . . . . . 8 (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
3121, 30orbi12d 914 . . . . . . 7 (𝑜 = ⟨𝑒, 𝑏⟩ → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)})) ↔ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
3210, 31rexopabb 5411 . . . . . 6 (∃𝑜 ∈ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)})) ↔ ∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
339, 32syl6bb 288 . . . . 5 ((𝑀𝑉𝐸𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)})) ↔ ∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
345satfv0 32491 . . . . . . . . . . 11 ((𝑀𝑉𝐸𝑊) → (𝑆‘∅) = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})})
3534rexeqdv 3421 . . . . . . . . . 10 ((𝑀𝑉𝐸𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ↔ ∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})} (𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝))))))
36 eqid 2825 . . . . . . . . . . 11 {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})} = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})}
37 vex 3502 . . . . . . . . . . . . . . 15 𝑐 ∈ V
38 vex 3502 . . . . . . . . . . . . . . 15 𝑑 ∈ V
3937, 38op1std 7693 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑐, 𝑑⟩ → (1st𝑝) = 𝑐)
4039oveq2d 7167 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑒𝑔(1st𝑝)) = (𝑒𝑔𝑐))
4140eqeq2d 2836 . . . . . . . . . . . 12 (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑥 = (𝑒𝑔(1st𝑝)) ↔ 𝑥 = (𝑒𝑔𝑐)))
4237, 38op2ndd 7694 . . . . . . . . . . . . . . 15 (𝑝 = ⟨𝑐, 𝑑⟩ → (2nd𝑝) = 𝑑)
4342ineq2d 4192 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑏 ∩ (2nd𝑝)) = (𝑏𝑑))
4443difeq2d 4102 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝))) = ((𝑀m ω) ∖ (𝑏𝑑)))
4544eqeq2d 2836 . . . . . . . . . . . 12 (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝))) ↔ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑))))
4641, 45anbi12d 630 . . . . . . . . . . 11 (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ↔ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))))
4736, 46rexopabb 5411 . . . . . . . . . 10 (∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})} (𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ↔ ∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))))
4835, 47syl6bb 288 . . . . . . . . 9 ((𝑀𝑉𝐸𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ↔ ∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑))))))
4948orbi1d 912 . . . . . . . 8 ((𝑀𝑉𝐸𝑊) → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
5049anbi2d 628 . . . . . . 7 ((𝑀𝑉𝐸𝑊) → ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
51502exbidv 1918 . . . . . 6 ((𝑀𝑉𝐸𝑊) → (∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
52 r19.41vv 3353 . . . . . . . . 9 (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
53 oveq1 7158 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖𝑔𝑗) → (𝑒𝑔𝑐) = ((𝑖𝑔𝑗)⊼𝑔𝑐))
5453eqeq2d 2836 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖𝑔𝑗) → (𝑥 = (𝑒𝑔𝑐) ↔ 𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐)))
55 ineq1 4184 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → (𝑏𝑑) = ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))
5655difeq2d 4102 . . . . . . . . . . . . . . . . . . 19 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → ((𝑀m ω) ∖ (𝑏𝑑)) = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))
5756eqeq2d 2836 . . . . . . . . . . . . . . . . . 18 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → (𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)) ↔ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))))
5854, 57bi2anan9 635 . . . . . . . . . . . . . . . . 17 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → ((𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑))) ↔ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
5958anbi2d 628 . . . . . . . . . . . . . . . 16 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))))))
60592exbidv 1918 . . . . . . . . . . . . . . 15 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ↔ ∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))))))
61 eqidd 2826 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖𝑔𝑗) → 𝑛 = 𝑛)
62 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖𝑔𝑗) → 𝑒 = (𝑖𝑔𝑗))
6361, 62goaleq12d 32484 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖𝑔𝑗) → ∀𝑔𝑛𝑒 = ∀𝑔𝑛(𝑖𝑔𝑗))
6463eqeq2d 2836 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖𝑔𝑗) → (𝑥 = ∀𝑔𝑛𝑒𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗)))
65 nfrab1 3389 . . . . . . . . . . . . . . . . . . . 20 𝑎{𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}
6665nfeq2 2999 . . . . . . . . . . . . . . . . . . 19 𝑎 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}
67 eleq2 2905 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}))
6867ralbidv 3201 . . . . . . . . . . . . . . . . . . 19 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → (∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}))
6966, 68rabbid 3480 . . . . . . . . . . . . . . . . . 18 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})
7069eqeq2d 2836 . . . . . . . . . . . . . . . . 17 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))
7164, 70bi2anan9 635 . . . . . . . . . . . . . . . 16 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → ((𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})))
7271rexbidv 3301 . . . . . . . . . . . . . . 15 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})))
7360, 72orbi12d 914 . . . . . . . . . . . . . 14 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → ((∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))))
7473adantl 482 . . . . . . . . . . . . 13 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})) → ((∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))))
75 r19.41vv 3353 . . . . . . . . . . . . . . . . 17 (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
76 oveq2 7159 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑘𝑔𝑙) → ((𝑖𝑔𝑗)⊼𝑔𝑐) = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)))
7776adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → ((𝑖𝑔𝑗)⊼𝑔𝑐) = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)))
7877eqeq2d 2836 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ↔ 𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙))))
79 ineq2 4186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} → ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}))
8079difeq2d 4102 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} → ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)) = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})))
81 inrab 4278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) = {𝑎 ∈ (𝑀m ω) ∣ ((𝑎𝑖)𝐸(𝑎𝑗) ∧ (𝑎𝑘)𝐸(𝑎𝑙))}
8281difeq2i 4099 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})) = ((𝑀m ω) ∖ {𝑎 ∈ (𝑀m ω) ∣ ((𝑎𝑖)𝐸(𝑎𝑗) ∧ (𝑎𝑘)𝐸(𝑎𝑙))})
83 notrab 4283 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀m ω) ∖ {𝑎 ∈ (𝑀m ω) ∣ ((𝑎𝑖)𝐸(𝑎𝑗) ∧ (𝑎𝑘)𝐸(𝑎𝑙))}) = {𝑎 ∈ (𝑀m ω) ∣ ¬ ((𝑎𝑖)𝐸(𝑎𝑗) ∧ (𝑎𝑘)𝐸(𝑎𝑙))}
84 ianor 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ ((𝑎𝑖)𝐸(𝑎𝑗) ∧ (𝑎𝑘)𝐸(𝑎𝑙)) ↔ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙)))
8584rabbii 3478 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑎 ∈ (𝑀m ω) ∣ ¬ ((𝑎𝑖)𝐸(𝑎𝑗) ∧ (𝑎𝑘)𝐸(𝑎𝑙))} = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}
8682, 83, 853eqtri 2852 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}
8780, 86syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} → ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))})
8887eqeq2d 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} → (𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
8988adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → (𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
9078, 89anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → ((𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))})))
9190biimpa 477 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) → (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
9291reximi 3247 . . . . . . . . . . . . . . . . . 18 (∃𝑙 ∈ ω ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
9392reximi 3247 . . . . . . . . . . . . . . . . 17 (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
9475, 93sylbir 236 . . . . . . . . . . . . . . . 16 ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
9594exlimivv 1926 . . . . . . . . . . . . . . 15 (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}))
9695a1i 11 . . . . . . . . . . . . . 14 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})) → (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))})))
97 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
98 simpll 763 . . . . . . . . . . . . . . . . . . . 20 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
99 simplr 765 . . . . . . . . . . . . . . . . . . . 20 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
100 fveq1 6665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑏 → (𝑎𝑖) = (𝑏𝑖))
101 fveq1 6665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑏 → (𝑎𝑗) = (𝑏𝑗))
102100, 101breq12d 5075 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑏 → ((𝑎𝑖)𝐸(𝑎𝑗) ↔ (𝑏𝑖)𝐸(𝑏𝑗)))
103102cbvrabv 3496 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑏 ∈ (𝑀m ω) ∣ (𝑏𝑖)𝐸(𝑏𝑗)}
104103eleq2i 2908 . . . . . . . . . . . . . . . . . . . . . . 23 (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀m ω) ∣ (𝑏𝑖)𝐸(𝑏𝑗)})
105104ralbii 3169 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ↔ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀m ω) ∣ (𝑏𝑖)𝐸(𝑏𝑗)})
106105rabbii 3478 . . . . . . . . . . . . . . . . . . . . 21 {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀m ω) ∣ (𝑏𝑖)𝐸(𝑏𝑗)}}
107 satfv1lem 32495 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀m ω) ∣ (𝑏𝑖)𝐸(𝑏𝑗)}} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})
108106, 107syl5eq 2872 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})
10997, 98, 99, 108syl3anc 1365 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})
110109eqeq2d 2836 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}} ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))
111110biimpd 230 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}} → 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))
112111anim2d 611 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}) → (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
113112reximdva 3278 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
114113adantr 481 . . . . . . . . . . . . . 14 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
11596, 114orim12d 960 . . . . . . . . . . . . 13 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})) → ((∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))))
11674, 115sylbid 241 . . . . . . . . . . . 12 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})) → ((∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))))
117116expimpd 454 . . . . . . . . . . 11 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))))
118117reximdva 3278 . . . . . . . . . 10 (𝑖 ∈ ω → (∃𝑗 ∈ ω ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))))
119118reximia 3246 . . . . . . . . 9 (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
12052, 119sylbir 236 . . . . . . . 8 ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
121120exlimivv 1926 . . . . . . 7 (∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
122 ovex 7184 . . . . . . . . . . . . 13 (𝑖𝑔𝑗) ∈ V
123 ovex 7184 . . . . . . . . . . . . . 14 (𝑀m ω) ∈ V
124123rabex 5231 . . . . . . . . . . . . 13 {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∈ V
125122, 124pm3.2i 471 . . . . . . . . . . . 12 ((𝑖𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∈ V)
126 eqid 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑔𝑙) = (𝑘𝑔𝑙)
127 eqid 2825 . . . . . . . . . . . . . . . . . . . . 21 {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}
128126, 127pm3.2i 471 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑔𝑙) = (𝑘𝑔𝑙) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})
12986eqcomi 2834 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))} = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}))
130129eqeq2i 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))} ↔ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})))
131130biimpi 217 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))} → 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})))
132131anim2i 616 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) → (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}))))
133 ovex 7184 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑔𝑙) ∈ V
134123rabex 5231 . . . . . . . . . . . . . . . . . . . . 21 {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} ∈ V
135 eqeq1 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑘𝑔𝑙) → (𝑐 = (𝑘𝑔𝑙) ↔ (𝑘𝑔𝑙) = (𝑘𝑔𝑙)))
136 eqeq1 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} → (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} ↔ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}))
137135, 136bi2anan9 635 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ↔ ((𝑘𝑔𝑙) = (𝑘𝑔𝑙) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})))
13876eqeq2d 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑘𝑔𝑙) → (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ↔ 𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙))))
13980eqeq2d 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} → (𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)) ↔ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}))))
140138, 139bi2anan9 635 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → ((𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})))))
141137, 140anbi12d 630 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) → (((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ↔ (((𝑘𝑔𝑙) = (𝑘𝑔𝑙) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}))))))
142133, 134, 141spc2ev 3611 . . . . . . . . . . . . . . . . . . . 20 ((((𝑘𝑔𝑙) = (𝑘𝑔𝑙) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)})))) → ∃𝑐𝑑((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
143128, 132, 142sylancr 587 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) → ∃𝑐𝑑((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
144143reximi 3247 . . . . . . . . . . . . . . . . . 18 (∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) → ∃𝑙 ∈ ω ∃𝑐𝑑((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
145144reximi 3247 . . . . . . . . . . . . . . . . 17 (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐𝑑((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
14675bicomi 225 . . . . . . . . . . . . . . . . . . 19 ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
1471462exbii 1842 . . . . . . . . . . . . . . . . . 18 (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ↔ ∃𝑐𝑑𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
148 2ex2rexrot 3254 . . . . . . . . . . . . . . . . . 18 (∃𝑐𝑑𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐𝑑((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
149147, 148bitri 276 . . . . . . . . . . . . . . . . 17 (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐𝑑((𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
150145, 149sylibr 235 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) → ∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))))
151150a1i 11 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) → ∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑))))))
152109eqcomd 2831 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))} = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})
153152eqeq2d 2836 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))} ↔ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))
154153biimpd 230 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))} → 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))
155154anim2d 611 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}) → (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})))
156155reximdva 3278 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}) → ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})))
157151, 156orim12d 960 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})) → (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))))
158157imp 407 . . . . . . . . . . . . 13 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))) → (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})))
159 eqid 2825 . . . . . . . . . . . . . 14 (𝑖𝑔𝑗) = (𝑖𝑔𝑗)
160 eqid 2825 . . . . . . . . . . . . . 14 {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}
161159, 160pm3.2i 471 . . . . . . . . . . . . 13 ((𝑖𝑔𝑗) = (𝑖𝑔𝑗) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})
162158, 161jctil 520 . . . . . . . . . . . 12 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))) → (((𝑖𝑔𝑗) = (𝑖𝑔𝑗) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))))
163 eqeq1 2829 . . . . . . . . . . . . . . 15 (𝑒 = (𝑖𝑔𝑗) → (𝑒 = (𝑖𝑔𝑗) ↔ (𝑖𝑔𝑗) = (𝑖𝑔𝑗)))
164 eqeq1 2829 . . . . . . . . . . . . . . 15 (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} → (𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ↔ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}))
165163, 164bi2anan9 635 . . . . . . . . . . . . . 14 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ↔ ((𝑖𝑔𝑗) = (𝑖𝑔𝑗) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})))
166165, 73anbi12d 630 . . . . . . . . . . . . 13 ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) → (((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (((𝑖𝑔𝑗) = (𝑖𝑔𝑗) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}})))))
167166spc2egv 3603 . . . . . . . . . . . 12 (((𝑖𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∈ V) → ((((𝑖𝑔𝑗) = (𝑖𝑔𝑗) ∧ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = ((𝑖𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ ({𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}}))) → ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
168125, 162, 167mpsyl 68 . . . . . . . . . . 11 (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))) → ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
169168ex 413 . . . . . . . . . 10 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})) → ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
170169reximdva 3278 . . . . . . . . 9 (𝑖 ∈ ω → (∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
171170reximia 3246 . . . . . . . 8 (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
17252bicomi 225 . . . . . . . . . 10 ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
1731722exbii 1842 . . . . . . . . 9 (∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒𝑏𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
174 2ex2rexrot 3254 . . . . . . . . 9 (∃𝑒𝑏𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
175173, 174bitri 276 . . . . . . . 8 (∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒𝑏((𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
176171, 175sylibr 235 . . . . . . 7 (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})) → ∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
177121, 176impbii 210 . . . . . 6 (∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑐𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑘)𝐸(𝑎𝑙)}) ∧ (𝑥 = (𝑒𝑔𝑐) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))})))
17851, 177syl6bb 288 . . . . 5 ((𝑀𝑉𝐸𝑊) → (∃𝑒𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ (𝑏 ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))))
17933, 178bitrd 280 . . . 4 ((𝑀𝑉𝐸𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))))
180179opabbidv 5128 . . 3 ((𝑀𝑉𝐸𝑊) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))})
181180uneq2d 4142 . 2 ((𝑀𝑉𝐸𝑊) → ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st𝑜)⊼𝑔(1st𝑝)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑜) ∩ (2nd𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd𝑜)}))}) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))}))
1823, 7, 1813eqtrd 2864 1 ((𝑀𝑉𝐸𝑊) → (𝑆‘1o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖𝑔𝑗)⊼𝑔(𝑘𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝑖)𝐸(𝑎𝑗) ∨ ¬ (𝑎𝑘)𝐸(𝑎𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎𝑗)), if-(𝑗 = 𝑛, (𝑎𝑖)𝐸𝑧, (𝑎𝑖)𝐸(𝑎𝑗)))}))}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 843  if-wif 1056   ∧ w3a 1081   = wceq 1530  ∃wex 1773   ∈ wcel 2107  ∀wral 3142  ∃wrex 3143  {crab 3146  Vcvv 3499   ∖ cdif 3936   ∪ cun 3937   ∩ cin 3938  ∅c0 4294  {csn 4563  ⟨cop 4569   class class class wbr 5062  {copab 5124   ↾ cres 5555  suc csuc 6190  ‘cfv 6351  (class class class)co 7151  ωcom 7571  1st c1st 7681  2nd c2nd 7682  1oc1o 8089   ↑m cmap 8399  ∈𝑔cgoe 32466  ⊼𝑔cgna 32467  ∀𝑔cgol 32468   Sat csat 32469 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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ifp 1057  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-map 8401  df-goel 32473  df-goal 32475  df-sat 32476 This theorem is referenced by:  satfv1fvfmla1  32556
 Copyright terms: Public domain W3C validator