Step | Hyp | Ref
| Expression |
1 | | df-1o 8297 |
. . . 4
⊢
1o = suc ∅ |
2 | 1 | fveq2i 6777 |
. . 3
⊢ (𝑆‘1o) = (𝑆‘suc
∅) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1o) = (𝑆‘suc ∅)) |
4 | | peano1 7735 |
. . 3
⊢ ∅
∈ ω |
5 | | satfv1.s |
. . . 4
⊢ 𝑆 = (𝑀 Sat 𝐸) |
6 | 5 | satfvsuc 33323 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪
{〈𝑥, 𝑦〉 ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)}))})) |
7 | 4, 6 | mp3an3 1449 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)}))})) |
8 | 5 | satfv0 33320 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {〈𝑒, 𝑏〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) |
9 | 8 | rexeqdv 3349 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)})) ↔ ∃𝑜 ∈ {〈𝑒, 𝑏〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)})))) |
10 | | eqid 2738 |
. . . . . . 7
⊢
{〈𝑒, 𝑏〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {〈𝑒, 𝑏〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} |
11 | | vex 3436 |
. . . . . . . . . . . . 13
⊢ 𝑒 ∈ V |
12 | | vex 3436 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ V |
13 | 11, 12 | op1std 7841 |
. . . . . . . . . . . 12
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (1st ‘𝑜) = 𝑒) |
14 | 13 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (𝑜 = 〈𝑒, 𝑏〉 → ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) = (𝑒⊼𝑔(1st
‘𝑝))) |
15 | 14 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ↔ 𝑥 = (𝑒⊼𝑔(1st
‘𝑝)))) |
16 | 11, 12 | op2ndd 7842 |
. . . . . . . . . . . . 13
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (2nd ‘𝑜) = 𝑏) |
17 | 16 | ineq1d 4145 |
. . . . . . . . . . . 12
⊢ (𝑜 = 〈𝑒, 𝑏〉 → ((2nd ‘𝑜) ∩ (2nd
‘𝑝)) = (𝑏 ∩ (2nd
‘𝑝))) |
18 | 17 | difeq2d 4057 |
. . . . . . . . . . 11
⊢ (𝑜 = 〈𝑒, 𝑏〉 → ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝))) = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) |
19 | 18 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝))))) |
20 | 15, 19 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑒, 𝑏〉 → ((𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))))) |
21 | 20 | rexbidv 3226 |
. . . . . . . 8
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))))) |
22 | | eqidd 2739 |
. . . . . . . . . . . 12
⊢ (𝑜 = 〈𝑒, 𝑏〉 → 𝑛 = 𝑛) |
23 | 22, 13 | goaleq12d 33313 |
. . . . . . . . . . 11
⊢ (𝑜 = 〈𝑒, 𝑏〉 →
∀𝑔𝑛(1st ‘𝑜) = ∀𝑔𝑛𝑒) |
24 | 23 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ↔ 𝑥 = ∀𝑔𝑛𝑒)) |
25 | 16 | eleq2d 2824 |
. . . . . . . . . . . . 13
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜) ↔ ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏)) |
26 | 25 | ralbidv 3112 |
. . . . . . . . . . . 12
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜) ↔ ∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏)) |
27 | 26 | rabbidv 3414 |
. . . . . . . . . . 11
⊢ (𝑜 = 〈𝑒, 𝑏〉 → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) |
28 | 27 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) |
29 | 24, 28 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑒, 𝑏〉 → ((𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)}) ↔ (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) |
30 | 29 | rexbidv 3226 |
. . . . . . . 8
⊢ (𝑜 = 〈𝑒, 𝑏〉 → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)}) ↔ ∃𝑛 ∈ ω (𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) |
31 | 21, 30 | orbi12d 916 |
. . . . . . 7
⊢ (𝑜 = 〈𝑒, 𝑏〉 → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)})) ↔ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
32 | 10, 31 | rexopabb 5441 |
. . . . . 6
⊢
(∃𝑜 ∈
{〈𝑒, 𝑏〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)})) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
33 | 9, 32 | bitrdi 287 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)})) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))) |
34 | 5 | satfv0 33320 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {〈𝑐, 𝑑〉 ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})}) |
35 | 34 | rexeqdv 3349 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ↔
∃𝑝 ∈
{〈𝑐, 𝑑〉 ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))))) |
36 | | eqid 2738 |
. . . . . . . . . . 11
⊢
{〈𝑐, 𝑑〉 ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} = {〈𝑐, 𝑑〉 ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} |
37 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑐 ∈ V |
38 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑑 ∈ V |
39 | 37, 38 | op1std 7841 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑐, 𝑑〉 → (1st ‘𝑝) = 𝑐) |
40 | 39 | oveq2d 7291 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑐, 𝑑〉 → (𝑒⊼𝑔(1st
‘𝑝)) = (𝑒⊼𝑔𝑐)) |
41 | 40 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑐, 𝑑〉 → (𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ↔ 𝑥 = (𝑒⊼𝑔𝑐))) |
42 | 37, 38 | op2ndd 7842 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈𝑐, 𝑑〉 → (2nd ‘𝑝) = 𝑑) |
43 | 42 | ineq2d 4146 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑐, 𝑑〉 → (𝑏 ∩ (2nd ‘𝑝)) = (𝑏 ∩ 𝑑)) |
44 | 43 | difeq2d 4057 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑐, 𝑑〉 → ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝))) = ((𝑀 ↑m ω)
∖ (𝑏 ∩ 𝑑))) |
45 | 44 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑐, 𝑑〉 → (𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝))) ↔ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) |
46 | 41, 45 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑐, 𝑑〉 → ((𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ↔ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑))))) |
47 | 36, 46 | rexopabb 5441 |
. . . . . . . . . 10
⊢
(∃𝑝 ∈
{〈𝑐, 𝑑〉 ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ↔
∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑))))) |
48 | 35, 47 | bitrdi 287 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ↔
∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))))) |
49 | 48 | orbi1d 914 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
50 | 49 | anbi2d 629 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))) |
51 | 50 | 2exbidv 1927 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))) |
52 | | r19.41vv 3278 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
53 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖∈𝑔𝑗) → (𝑒⊼𝑔𝑐) = ((𝑖∈𝑔𝑗)⊼𝑔𝑐)) |
54 | 53 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖∈𝑔𝑗) → (𝑥 = (𝑒⊼𝑔𝑐) ↔ 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐))) |
55 | | ineq1 4139 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) |
56 | 55 | difeq2d 4057 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)) = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) |
57 | 56 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) |
58 | 54, 57 | bi2anan9 636 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
59 | 58 | anbi2d 629 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))) |
60 | 59 | 2exbidv 1927 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))) |
61 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖∈𝑔𝑗) → 𝑛 = 𝑛) |
62 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖∈𝑔𝑗) → 𝑒 = (𝑖∈𝑔𝑗)) |
63 | 61, 62 | goaleq12d 33313 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖∈𝑔𝑗) → ∀𝑔𝑛𝑒 = ∀𝑔𝑛(𝑖∈𝑔𝑗)) |
64 | 63 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝑖∈𝑔𝑗) → (𝑥 = ∀𝑔𝑛𝑒 ↔ 𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗))) |
65 | | nfrab1 3317 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑎{𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} |
66 | 65 | nfeq2 2924 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑎 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} |
67 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
68 | 67 | ralbidv 3112 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
69 | 66, 68 | rabbid 3410 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) |
70 | 69 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) |
71 | 64, 70 | bi2anan9 636 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) |
72 | 71 | rexbidv 3226 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) |
73 | 60, 72 | orbi12d 916 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))) |
74 | 73 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))) |
75 | | r19.41vv 3278 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑘 ∈
ω ∃𝑙 ∈
ω ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
76 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑘∈𝑔𝑙) → ((𝑖∈𝑔𝑗)⊼𝑔𝑐) = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙))) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑖∈𝑔𝑗)⊼𝑔𝑐) = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙))) |
78 | 77 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ↔ 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)))) |
79 | | ineq2 4140 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) |
80 | 79 | difeq2d 4057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))) |
81 | | inrab 4240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) = {𝑎 ∈ (𝑀 ↑m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} |
82 | 81 | difeq2i 4054 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ↑m ω)
∖ ({𝑎 ∈ (𝑀 ↑m ω)
∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = ((𝑀 ↑m ω) ∖ {𝑎 ∈ (𝑀 ↑m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) |
83 | | notrab 4245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ↑m ω)
∖ {𝑎 ∈ (𝑀 ↑m ω)
∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) = {𝑎 ∈ (𝑀 ↑m ω) ∣ ¬
((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} |
84 | | ianor 979 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))) |
85 | 84 | rabbii 3408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ¬
((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} |
86 | 82, 83, 85 | 3eqtri 2770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 ↑m ω)
∖ ({𝑎 ∈ (𝑀 ↑m ω)
∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} |
87 | 80, 86 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) |
88 | 87 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
90 | 78, 89 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) |
91 | 90 | biimpa 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
92 | 91 | reximi 3178 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑙 ∈
ω ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
93 | 92 | reximi 3178 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑘 ∈
ω ∃𝑙 ∈
ω ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
94 | 75, 93 | sylbir 234 |
. . . . . . . . . . . . . . . 16
⊢
((∃𝑘 ∈
ω ∃𝑙 ∈
ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
95 | 94 | exlimivv 1935 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) |
97 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑛 ∈
ω) |
98 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑖 ∈
ω) |
99 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑗 ∈
ω) |
100 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑏 → (𝑎‘𝑖) = (𝑏‘𝑖)) |
101 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑏 → (𝑎‘𝑗) = (𝑏‘𝑗)) |
102 | 100, 101 | breq12d 5087 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑏 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑏‘𝑖)𝐸(𝑏‘𝑗))) |
103 | 102 | cbvrabv 3426 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)} |
104 | 103 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}) |
105 | 104 | ralbii 3092 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑧 ∈
𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}) |
106 | 105 | rabbii 3408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} |
107 | | satfv1lem 33324 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) |
108 | 106, 107 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) |
109 | 97, 98, 99, 108 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) |
110 | 109 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) |
111 | 110 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} → 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) |
112 | 111 | anim2d 612 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 =
∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
113 | 112 | reximdva 3203 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
(∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
114 | 113 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
115 | 96, 114 | orim12d 962 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) |
116 | 74, 115 | sylbid 239 |
. . . . . . . . . . . 12
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) |
117 | 116 | expimpd 454 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) |
118 | 117 | reximdva 3203 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ω →
(∃𝑗 ∈ ω
((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) |
119 | 118 | reximia 3176 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
120 | 52, 119 | sylbir 234 |
. . . . . . . 8
⊢
((∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
121 | 120 | exlimivv 1935 |
. . . . . . 7
⊢
(∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
122 | | ovex 7308 |
. . . . . . . . . . . . 13
⊢ (𝑖∈𝑔𝑗) ∈ V |
123 | | ovex 7308 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↑m ω)
∈ V |
124 | 123 | rabex 5256 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V |
125 | 122, 124 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ ((𝑖∈𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V) |
126 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘∈𝑔𝑙) = (𝑘∈𝑔𝑙) |
127 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} |
128 | 126, 127 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘∈𝑔𝑙) = (𝑘∈𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) |
129 | 86 | eqcomi 2747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) |
130 | 129 | eqeq2i 2751 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))) |
131 | 130 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} → 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))) |
132 | 131 | anim2i 617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) |
133 | | ovex 7308 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘∈𝑔𝑙) ∈ V |
134 | 123 | rabex 5256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ∈ V |
135 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑘∈𝑔𝑙) → (𝑐 = (𝑘∈𝑔𝑙) ↔ (𝑘∈𝑔𝑙) = (𝑘∈𝑔𝑙))) |
136 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) |
137 | 135, 136 | bi2anan9 636 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ↔ ((𝑘∈𝑔𝑙) = (𝑘∈𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))) |
138 | 76 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑘∈𝑔𝑙) → (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ↔ 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)))) |
139 | 80 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) |
140 | 138, 139 | bi2anan9 636 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))) |
141 | 137, 140 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (((𝑘∈𝑔𝑙) = (𝑘∈𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))))) |
142 | 133, 134,
141 | spc2ev 3546 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑘∈𝑔𝑙) = (𝑘∈𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) → ∃𝑐∃𝑑((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
143 | 128, 132,
142 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
144 | 143 | reximi 3178 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑙 ∈
ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
145 | 144 | reximi 3178 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑘 ∈
ω ∃𝑙 ∈
ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
146 | 75 | bicomi 223 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃𝑘 ∈
ω ∃𝑙 ∈
ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
147 | 146 | 2exbii 1851 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
148 | | 2ex2rexrot 3235 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
149 | 147, 148 | bitri 274 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
150 | 145, 149 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑘 ∈
ω ∃𝑙 ∈
ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
(∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))) |
152 | 109 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) |
153 | 152 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) |
154 | 153 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} → 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) |
155 | 154 | anim2d 612 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 =
∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) |
156 | 155 | reximdva 3203 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
(∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) |
157 | 151, 156 | orim12d 962 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
((∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))) |
158 | 157 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧
(∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) |
159 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗) |
160 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} |
161 | 159, 160 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ ((𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) |
162 | 158, 161 | jctil 520 |
. . . . . . . . . . . 12
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧
(∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (((𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))) |
163 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑖∈𝑔𝑗) → (𝑒 = (𝑖∈𝑔𝑗) ↔ (𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗))) |
164 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
165 | 163, 164 | bi2anan9 636 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
166 | 165, 73 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (((𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))) |
167 | 166 | spc2egv 3538 |
. . . . . . . . . . . 12
⊢ (((𝑖∈𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V) → ((((𝑖∈𝑔𝑗) = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ({𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))) |
168 | 125, 162,
167 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧
(∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
169 | 168 | ex 413 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
((∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))) |
170 | 169 | reximdva 3203 |
. . . . . . . . 9
⊢ (𝑖 ∈ ω →
(∃𝑗 ∈ ω
(∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))) |
171 | 170 | reximia 3176 |
. . . . . . . 8
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (∃𝑘 ∈
ω ∃𝑙 ∈
ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
172 | 52 | bicomi 223 |
. . . . . . . . . 10
⊢
((∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
173 | 172 | 2exbii 1851 |
. . . . . . . . 9
⊢
(∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
174 | | 2ex2rexrot 3235 |
. . . . . . . . 9
⊢
(∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
175 | 173, 174 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
176 | 171, 175 | sylibr 233 |
. . . . . . 7
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (∃𝑘 ∈
ω ∃𝑙 ∈
ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))) |
177 | 121, 176 | impbii 208 |
. . . . . 6
⊢
(∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) |
178 | 51, 177 | bitrdi 287 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ (𝑏 ∩ (2nd
‘𝑝)))) ∨
∃𝑛 ∈ ω
(𝑥 =
∀𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) |
179 | 33, 178 | bitrd 278 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) |
180 | 179 | opabbidv 5140 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {〈𝑥, 𝑦〉 ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)}))} = {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}) |
181 | 180 | uneq2d 4097 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑆‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1st ‘𝑜)⊼𝑔(1st
‘𝑝)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑜)
∩ (2nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(1st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑛, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2nd ‘𝑜)}))}) = ((𝑆‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})) |
182 | 3, 7, 181 | 3eqtrd 2782 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1o) = ((𝑆‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})) |