| Step | Hyp | Ref
| Expression |
| 1 | | satefv 35419 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (𝑀 Sat∈ 𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋)) |
| 2 | | incom 4209 |
. . . . . . . . 9
⊢ ( E ∩
(𝑀 × 𝑀)) = ((𝑀 × 𝑀) ∩ E ) |
| 3 | | sqxpexg 7775 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝑉 → (𝑀 × 𝑀) ∈ V) |
| 4 | | inex1g 5319 |
. . . . . . . . . 10
⊢ ((𝑀 × 𝑀) ∈ V → ((𝑀 × 𝑀) ∩ E ) ∈ V) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝑉 → ((𝑀 × 𝑀) ∩ E ) ∈ V) |
| 6 | 2, 5 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑉 → ( E ∩ (𝑀 × 𝑀)) ∈ V) |
| 7 | 6 | ancli 548 |
. . . . . . 7
⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ 𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V)) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (𝑀 ∈ 𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V)) |
| 9 | | satom 35361 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω) = ∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)) |
| 10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω) = ∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)) |
| 11 | 10 | fveq1d 6908 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
(((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋) = (∪
𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)‘𝑋)) |
| 12 | | satfun 35416 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω):(Fmla‘ω)⟶𝒫
(𝑀 ↑m
ω)) |
| 13 | 8, 12 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω):(Fmla‘ω)⟶𝒫
(𝑀 ↑m
ω)) |
| 14 | 13 | ffund 6740 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → Fun
((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)) |
| 15 | 10 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) = ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)) |
| 16 | 15 | funeqd 6588 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (Fun
∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) ↔ Fun ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω))) |
| 17 | 14, 16 | mpbird 257 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → Fun
∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)) |
| 18 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 19 | 18 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → ∅
∈ ω) |
| 20 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝑉 → ∅ ∈
ω) |
| 21 | | satfdmfmla 35405 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V ∧ ∅ ∈ ω)
→ dom ((𝑀 Sat ( E
∩ (𝑀 × 𝑀)))‘∅) =
(Fmla‘∅)) |
| 22 | 6, 20, 21 | mpd3an23 1465 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑉 → dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅) =
(Fmla‘∅)) |
| 23 | 22 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑀 ∈ 𝑉 → (Fmla‘∅) = dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)) |
| 24 | 23 | eleq2d 2827 |
. . . . . 6
⊢ (𝑀 ∈ 𝑉 → (𝑋 ∈ (Fmla‘∅) ↔ 𝑋 ∈ dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅))) |
| 25 | 24 | biimpa 476 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → 𝑋 ∈ dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)) |
| 26 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) = ∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) |
| 27 | 26 | fviunfun 7969 |
. . . . 5
⊢ ((Fun
∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) ∧ ∅ ∈ ω ∧ 𝑋 ∈ dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)) → (∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)‘𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)‘𝑋)) |
| 28 | 17, 19, 25, 27 | syl3anc 1373 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
(∪ 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)‘𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)‘𝑋)) |
| 29 | 11, 28 | eqtrd 2777 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
(((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)‘𝑋)) |
| 30 | | simpl 482 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → 𝑀 ∈ 𝑉) |
| 31 | 6 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → ( E
∩ (𝑀 × 𝑀)) ∈ V) |
| 32 | | simpr 484 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → 𝑋 ∈
(Fmla‘∅)) |
| 33 | | eqid 2737 |
. . . . . 6
⊢ (𝑀 Sat ( E ∩ (𝑀 × 𝑀))) = (𝑀 Sat ( E ∩ (𝑀 × 𝑀))) |
| 34 | 33 | satfv0fvfmla0 35418 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V ∧ 𝑋 ∈ (Fmla‘∅)) →
(((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋)))}) |
| 35 | 30, 31, 32, 34 | syl3anc 1373 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
(((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋)))}) |
| 36 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝑀 ↑m ω) → 𝑎:ω⟶𝑀) |
| 37 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑎:ω⟶𝑀 ∧ (𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅))) → 𝑎:ω⟶𝑀) |
| 38 | | fmla0xp 35388 |
. . . . . . . . . . . . . . . 16
⊢
(Fmla‘∅) = ({∅} × (ω ×
ω)) |
| 39 | 38 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (Fmla‘∅)
↔ 𝑋 ∈ ({∅}
× (ω × ω))) |
| 40 | | elxp 5708 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ({∅} ×
(ω × ω)) ↔ ∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω ×
ω)))) |
| 41 | 39, 40 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (Fmla‘∅)
↔ ∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω ×
ω)))) |
| 42 | | xp1st 8046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ω ×
ω) → (1st ‘𝑦) ∈ ω) |
| 43 | 42 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
(1st ‘𝑦)
∈ ω) |
| 44 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
| 45 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
| 46 | 44, 45 | op2ndd 8025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 = 〈𝑥, 𝑦〉 → (2nd ‘𝑋) = 𝑦) |
| 47 | 46 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 = 〈𝑥, 𝑦〉 → (1st
‘(2nd ‘𝑋)) = (1st ‘𝑦)) |
| 48 | 47 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 = 〈𝑥, 𝑦〉 → ((1st
‘(2nd ‘𝑋)) ∈ ω ↔ (1st
‘𝑦) ∈
ω)) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
((1st ‘(2nd ‘𝑋)) ∈ ω ↔ (1st
‘𝑦) ∈
ω)) |
| 50 | 43, 49 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
(1st ‘(2nd ‘𝑋)) ∈ ω) |
| 51 | 50 | exlimivv 1932 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
(1st ‘(2nd ‘𝑋)) ∈ ω) |
| 52 | 41, 51 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ (Fmla‘∅)
→ (1st ‘(2nd ‘𝑋)) ∈ ω) |
| 53 | 52 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝑎:ω⟶𝑀 ∧ (𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅))) →
(1st ‘(2nd ‘𝑋)) ∈ ω) |
| 54 | 37, 53 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝑎:ω⟶𝑀 ∧ (𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅))) → (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀) |
| 55 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ω ×
ω) → (2nd ‘𝑦) ∈ ω) |
| 56 | 55 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
(2nd ‘𝑦)
∈ ω) |
| 57 | 46 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 = 〈𝑥, 𝑦〉 → (2nd
‘(2nd ‘𝑋)) = (2nd ‘𝑦)) |
| 58 | 57 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 = 〈𝑥, 𝑦〉 → ((2nd
‘(2nd ‘𝑋)) ∈ ω ↔ (2nd
‘𝑦) ∈
ω)) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
((2nd ‘(2nd ‘𝑋)) ∈ ω ↔ (2nd
‘𝑦) ∈
ω)) |
| 60 | 56, 59 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
(2nd ‘(2nd ‘𝑋)) ∈ ω) |
| 61 | 60 | exlimivv 1932 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥∃𝑦(𝑋 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {∅} ∧ 𝑦 ∈ (ω × ω))) →
(2nd ‘(2nd ‘𝑋)) ∈ ω) |
| 62 | 41, 61 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ (Fmla‘∅)
→ (2nd ‘(2nd ‘𝑋)) ∈ ω) |
| 63 | 62 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝑎:ω⟶𝑀 ∧ (𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅))) →
(2nd ‘(2nd ‘𝑋)) ∈ ω) |
| 64 | 37, 63 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝑎:ω⟶𝑀 ∧ (𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅))) → (𝑎‘(2nd
‘(2nd ‘𝑋))) ∈ 𝑀) |
| 65 | 54, 64 | jca 511 |
. . . . . . . . . 10
⊢ ((𝑎:ω⟶𝑀 ∧ (𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅))) →
((𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀 ∧ (𝑎‘(2nd ‘(2nd
‘𝑋))) ∈ 𝑀)) |
| 66 | 65 | ex 412 |
. . . . . . . . 9
⊢ (𝑎:ω⟶𝑀 → ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀 ∧ (𝑎‘(2nd ‘(2nd
‘𝑋))) ∈ 𝑀))) |
| 67 | 36, 66 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ (𝑀 ↑m ω) → ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀 ∧ (𝑎‘(2nd ‘(2nd
‘𝑋))) ∈ 𝑀))) |
| 68 | 67 | impcom 407 |
. . . . . . 7
⊢ (((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) ∧ 𝑎 ∈ (𝑀 ↑m ω)) → ((𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀 ∧ (𝑎‘(2nd ‘(2nd
‘𝑋))) ∈ 𝑀)) |
| 69 | | brinxp 5764 |
. . . . . . . 8
⊢ (((𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀 ∧ (𝑎‘(2nd ‘(2nd
‘𝑋))) ∈ 𝑀) → ((𝑎‘(1st ‘(2nd
‘𝑋))) E (𝑎‘(2nd
‘(2nd ‘𝑋))) ↔ (𝑎‘(1st ‘(2nd
‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋))))) |
| 70 | 69 | bicomd 223 |
. . . . . . 7
⊢ (((𝑎‘(1st
‘(2nd ‘𝑋))) ∈ 𝑀 ∧ (𝑎‘(2nd ‘(2nd
‘𝑋))) ∈ 𝑀) → ((𝑎‘(1st ‘(2nd
‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘(1st
‘(2nd ‘𝑋))) E (𝑎‘(2nd ‘(2nd
‘𝑋))))) |
| 71 | 68, 70 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) ∧ 𝑎 ∈ (𝑀 ↑m ω)) → ((𝑎‘(1st
‘(2nd ‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘(1st
‘(2nd ‘𝑋))) E (𝑎‘(2nd ‘(2nd
‘𝑋))))) |
| 72 | | fvex 6919 |
. . . . . . 7
⊢ (𝑎‘(2nd
‘(2nd ‘𝑋))) ∈ V |
| 73 | 72 | epeli 5586 |
. . . . . 6
⊢ ((𝑎‘(1st
‘(2nd ‘𝑋))) E (𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd
‘𝑋)))) |
| 74 | 71, 73 | bitrdi 287 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) ∧ 𝑎 ∈ (𝑀 ↑m ω)) → ((𝑎‘(1st
‘(2nd ‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋))) ↔ (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd
‘𝑋))))) |
| 75 | 74 | rabbidva 3443 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋)))( E ∩ (𝑀 × 𝑀))(𝑎‘(2nd ‘(2nd
‘𝑋)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd
‘𝑋)))}) |
| 76 | 35, 75 | eqtrd 2777 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
(((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd
‘𝑋)))}) |
| 77 | 29, 76 | eqtrd 2777 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) →
(((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd
‘𝑋)))}) |
| 78 | 1, 77 | eqtrd 2777 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd
‘𝑋)))}) |