| Step | Hyp | Ref
| Expression |
| 1 | | satfv0fun 35376 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘∅)) |
| 2 | | satfv0fv.s |
. . . . . 6
⊢ 𝑆 = (𝑀 Sat 𝐸) |
| 3 | 2 | fveq1i 6907 |
. . . . 5
⊢ (𝑆‘∅) = ((𝑀 Sat 𝐸)‘∅) |
| 4 | 3 | funeqi 6587 |
. . . 4
⊢ (Fun
(𝑆‘∅) ↔
Fun ((𝑀 Sat 𝐸)‘∅)) |
| 5 | 1, 4 | sylibr 234 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun (𝑆‘∅)) |
| 6 | 5 | 3adant3 1133 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) → Fun
(𝑆‘∅)) |
| 7 | | fmla0 35387 |
. . . . . . . 8
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
| 8 | 7 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑋 ∈ (Fmla‘∅)
↔ 𝑋 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)}) |
| 9 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑋 = (𝑖∈𝑔𝑗))) |
| 10 | 9 | 2rexbidv 3222 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑋 = (𝑖∈𝑔𝑗))) |
| 11 | 10 | elrab 3692 |
. . . . . . 7
⊢ (𝑋 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} ↔ (𝑋 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑋 = (𝑖∈𝑔𝑗))) |
| 12 | 8, 11 | bitri 275 |
. . . . . 6
⊢ (𝑋 ∈ (Fmla‘∅)
↔ (𝑋 ∈ V ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑋 = (𝑖∈𝑔𝑗))) |
| 13 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑋 = (𝑖∈𝑔𝑗)) → 𝑋 = (𝑖∈𝑔𝑗)) |
| 14 | | goel 35352 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = 〈∅, 〈𝑖, 𝑗〉〉) |
| 15 | 14 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑋 = (𝑖∈𝑔𝑗) ↔ 𝑋 = 〈∅, 〈𝑖, 𝑗〉〉)) |
| 16 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → (1st
‘(2nd ‘𝑋)) = (1st ‘(2nd
‘〈∅, 〈𝑖, 𝑗〉〉))) |
| 17 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
∈ V |
| 18 | | opex 5469 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈𝑖, 𝑗〉 ∈ V |
| 19 | 17, 18 | op2nd 8023 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈∅, 〈𝑖, 𝑗〉〉) = 〈𝑖, 𝑗〉 |
| 20 | 19 | fveq2i 6909 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘(2nd ‘〈∅, 〈𝑖, 𝑗〉〉)) = (1st
‘〈𝑖, 𝑗〉) |
| 21 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑖 ∈ V |
| 22 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑗 ∈ V |
| 23 | 21, 22 | op1st 8022 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘〈𝑖, 𝑗〉) = 𝑖 |
| 24 | 20, 23 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢
(1st ‘(2nd ‘〈∅, 〈𝑖, 𝑗〉〉)) = 𝑖 |
| 25 | 16, 24 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → (1st
‘(2nd ‘𝑋)) = 𝑖) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → (𝑎‘(1st ‘(2nd
‘𝑋))) = (𝑎‘𝑖)) |
| 27 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → (2nd
‘(2nd ‘𝑋)) = (2nd ‘(2nd
‘〈∅, 〈𝑖, 𝑗〉〉))) |
| 28 | 19 | fveq2i 6909 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(2nd ‘〈∅, 〈𝑖, 𝑗〉〉)) = (2nd
‘〈𝑖, 𝑗〉) |
| 29 | 21, 22 | op2nd 8023 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘〈𝑖, 𝑗〉) = 𝑗 |
| 30 | 28, 29 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢
(2nd ‘(2nd ‘〈∅, 〈𝑖, 𝑗〉〉)) = 𝑗 |
| 31 | 27, 30 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → (2nd
‘(2nd ‘𝑋)) = 𝑗) |
| 32 | 31 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → (𝑎‘(2nd ‘(2nd
‘𝑋))) = (𝑎‘𝑗)) |
| 33 | 26, 32 | breq12d 5156 |
. . . . . . . . . . . . 13
⊢ (𝑋 = 〈∅, 〈𝑖, 𝑗〉〉 → ((𝑎‘(1st ‘(2nd
‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘𝑖)𝐸(𝑎‘𝑗))) |
| 34 | 15, 33 | biimtrdi 253 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑋 = (𝑖∈𝑔𝑗) → ((𝑎‘(1st ‘(2nd
‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘𝑖)𝐸(𝑎‘𝑗)))) |
| 35 | 34 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑋 = (𝑖∈𝑔𝑗)) → ((𝑎‘(1st ‘(2nd
‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘𝑖)𝐸(𝑎‘𝑗))) |
| 36 | 35 | rabbidv 3444 |
. . . . . . . . . 10
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑋 = (𝑖∈𝑔𝑗)) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) |
| 37 | 13, 36 | jca 511 |
. . . . . . . . 9
⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑋 = (𝑖∈𝑔𝑗)) → (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
| 38 | 37 | ex 412 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑋 = (𝑖∈𝑔𝑗) → (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
| 39 | 38 | reximdva 3168 |
. . . . . . 7
⊢ (𝑖 ∈ ω →
(∃𝑗 ∈ ω
𝑋 = (𝑖∈𝑔𝑗) → ∃𝑗 ∈ ω (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
| 40 | 39 | reximia 3081 |
. . . . . 6
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑋 = (𝑖∈𝑔𝑗) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
| 41 | 12, 40 | simplbiim 504 |
. . . . 5
⊢ (𝑋 ∈ (Fmla‘∅)
→ ∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
| 42 | 41 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) →
∃𝑖 ∈ ω
∃𝑗 ∈ ω
(𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
| 43 | | simp3 1139 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) → 𝑋 ∈
(Fmla‘∅)) |
| 44 | | ovex 7464 |
. . . . . 6
⊢ (𝑀 ↑m ω)
∈ V |
| 45 | 44 | rabex 5339 |
. . . . 5
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} ∈
V |
| 46 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) |
| 47 | 9, 46 | bi2anan9 638 |
. . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}) →
((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
| 48 | 47 | 2rexbidv 3222 |
. . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}) →
(∃𝑖 ∈ ω
∃𝑗 ∈ ω
(𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
| 49 | 48 | opelopabga 5538 |
. . . . 5
⊢ ((𝑋 ∈ (Fmla‘∅)
∧ {𝑎 ∈ (𝑀 ↑m ω)
∣ (𝑎‘(1st ‘(2nd
‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} ∈ V)
→ (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
{〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
| 50 | 43, 45, 49 | sylancl 586 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) →
(〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
{〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑋 = (𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))) |
| 51 | 42, 50 | mpbird 257 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) →
〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
{〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) |
| 52 | 2 | satfv0 35363 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) |
| 53 | 52 | eleq2d 2827 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
(𝑆‘∅) ↔
〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
{〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})) |
| 54 | 53 | 3adant3 1133 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) →
(〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
(𝑆‘∅) ↔
〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
{〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})) |
| 55 | 51, 54 | mpbird 257 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) →
〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
(𝑆‘∅)) |
| 56 | | funopfv 6958 |
. 2
⊢ (Fun
(𝑆‘∅) →
(〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}〉 ∈
(𝑆‘∅) →
((𝑆‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))})) |
| 57 | 6, 55, 56 | sylc 65 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑆‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd
‘𝑋)))}) |