| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢ (ω
× {𝑋}) = (ω
× {𝑋}) |
| 2 | | omex 9683 |
. . . . . . . 8
⊢ ω
∈ V |
| 3 | | snex 5436 |
. . . . . . . 8
⊢ {𝑋} ∈ V |
| 4 | 2, 3 | xpex 7773 |
. . . . . . 7
⊢ (ω
× {𝑋}) ∈
V |
| 5 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑎 = (ω × {𝑋}) → (𝑎 = (ω × {𝑋}) ↔ (ω × {𝑋}) = (ω × {𝑋}))) |
| 6 | 4, 5 | spcev 3606 |
. . . . . 6
⊢ ((ω
× {𝑋}) = (ω
× {𝑋}) →
∃𝑎 𝑎 = (ω × {𝑋})) |
| 7 | 1, 6 | mp1i 13 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ∃𝑎 𝑎 = (ω × {𝑋})) |
| 8 | 3, 2 | pm3.2i 470 |
. . . . . . . 8
⊢ ({𝑋} ∈ V ∧ ω ∈
V) |
| 9 | | elmapg 8879 |
. . . . . . . 8
⊢ (({𝑋} ∈ V ∧ ω ∈
V) → (𝑎 ∈ ({𝑋} ↑m ω)
↔ 𝑎:ω⟶{𝑋})) |
| 10 | 8, 9 | mp1i 13 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝑎 ∈ ({𝑋} ↑m ω) ↔ 𝑎:ω⟶{𝑋})) |
| 11 | | fconst2g 7223 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑎:ω⟶{𝑋} ↔ 𝑎 = (ω × {𝑋}))) |
| 12 | 11 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝑎:ω⟶{𝑋} ↔ 𝑎 = (ω × {𝑋}))) |
| 13 | 10, 12 | bitrd 279 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝑎 ∈ ({𝑋} ↑m ω) ↔ 𝑎 = (ω × {𝑋}))) |
| 14 | 13 | exbidv 1921 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (∃𝑎 𝑎 ∈ ({𝑋} ↑m ω) ↔
∃𝑎 𝑎 = (ω × {𝑋}))) |
| 15 | 7, 14 | mpbird 257 |
. . . 4
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ∃𝑎 𝑎 ∈ ({𝑋} ↑m
ω)) |
| 16 | | neq0 4352 |
. . . 4
⊢ (¬
({𝑋} ↑m
ω) = ∅ ↔ ∃𝑎 𝑎 ∈ ({𝑋} ↑m
ω)) |
| 17 | 15, 16 | sylibr 234 |
. . 3
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ ({𝑋} ↑m ω) =
∅) |
| 18 | | eqcom 2744 |
. . 3
⊢ (({𝑋} ↑m ω) =
∅ ↔ ∅ = ({𝑋} ↑m
ω)) |
| 19 | 17, 18 | sylnib 328 |
. 2
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ ∅ = ({𝑋} ↑m
ω)) |
| 20 | | ovex 7464 |
. . . . 5
⊢ (𝐼∈𝑔𝐽) ∈ V |
| 21 | 3, 20 | pm3.2i 470 |
. . . 4
⊢ ({𝑋} ∈ V ∧ (𝐼∈𝑔𝐽) ∈ V) |
| 22 | | prv 35433 |
. . . 4
⊢ (({𝑋} ∈ V ∧ (𝐼∈𝑔𝐽) ∈ V) → ({𝑋}⊧(𝐼∈𝑔𝐽) ↔ ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ({𝑋} ↑m
ω))) |
| 23 | 21, 22 | mp1i 13 |
. . 3
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋}⊧(𝐼∈𝑔𝐽) ↔ ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ({𝑋} ↑m
ω))) |
| 24 | | goel 35352 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) = 〈∅, 〈𝐼, 𝐽〉〉) |
| 25 | | 0ex 5307 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
| 26 | 25 | snid 4662 |
. . . . . . . . . . 11
⊢ ∅
∈ {∅} |
| 27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → ∅
∈ {∅}) |
| 28 | | opelxpi 5722 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
〈𝐼, 𝐽〉 ∈ (ω ×
ω)) |
| 29 | 27, 28 | opelxpd 5724 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
〈∅, 〈𝐼,
𝐽〉〉 ∈
({∅} × (ω × ω))) |
| 30 | 24, 29 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ ({∅} ×
(ω × ω))) |
| 31 | | fmla0xp 35388 |
. . . . . . . 8
⊢
(Fmla‘∅) = ({∅} × (ω ×
ω)) |
| 32 | 30, 31 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈
(Fmla‘∅)) |
| 33 | 32 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝐼∈𝑔𝐽) ∈
(Fmla‘∅)) |
| 34 | | satefvfmla0 35423 |
. . . . . 6
⊢ (({𝑋} ∈ V ∧ (𝐼∈𝑔𝐽) ∈ (Fmla‘∅))
→ ({𝑋}
Sat∈ (𝐼∈𝑔𝐽)) = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))}) |
| 35 | 3, 33, 34 | sylancr 587 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))}) |
| 36 | 24 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(𝐼∈𝑔𝐽)) = (2nd ‘〈∅,
〈𝐼, 𝐽〉〉)) |
| 37 | | opex 5469 |
. . . . . . . . . . . . . 14
⊢
〈𝐼, 𝐽〉 ∈ V |
| 38 | 25, 37 | op2nd 8023 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈∅, 〈𝐼, 𝐽〉〉) = 〈𝐼, 𝐽〉 |
| 39 | 36, 38 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(𝐼∈𝑔𝐽)) = 〈𝐼, 𝐽〉) |
| 40 | 39 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(1st ‘(2nd ‘(𝐼∈𝑔𝐽))) = (1st ‘〈𝐼, 𝐽〉)) |
| 41 | | op1stg 8026 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(1st ‘〈𝐼, 𝐽〉) = 𝐼) |
| 42 | 40, 41 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(1st ‘(2nd ‘(𝐼∈𝑔𝐽))) = 𝐼) |
| 43 | 42 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) = (𝑎‘𝐼)) |
| 44 | 39 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(2nd ‘(𝐼∈𝑔𝐽))) = (2nd ‘〈𝐼, 𝐽〉)) |
| 45 | | op2ndg 8027 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘〈𝐼, 𝐽〉) = 𝐽) |
| 46 | 44, 45 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(2nd ‘(𝐼∈𝑔𝐽))) = 𝐽) |
| 47 | 46 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝑎‘(2nd
‘(2nd ‘(𝐼∈𝑔𝐽)))) = (𝑎‘𝐽)) |
| 48 | 43, 47 | eleq12d 2835 |
. . . . . . . 8
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → ((𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽)))) ↔ (𝑎‘𝐼) ∈ (𝑎‘𝐽))) |
| 49 | 48 | rabbidv 3444 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))} = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)}) |
| 50 | 49 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))} = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)}) |
| 51 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ({𝑋} ↑m ω) → 𝑎:ω⟶{𝑋}) |
| 52 | | elirr 9637 |
. . . . . . . . . . . 12
⊢ ¬
𝑋 ∈ 𝑋 |
| 53 | | fvconst 7184 |
. . . . . . . . . . . . . 14
⊢ ((𝑎:ω⟶{𝑋} ∧ 𝐼 ∈ ω) → (𝑎‘𝐼) = 𝑋) |
| 54 | 53 | 3ad2antr1 1189 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → (𝑎‘𝐼) = 𝑋) |
| 55 | | fvconst 7184 |
. . . . . . . . . . . . . 14
⊢ ((𝑎:ω⟶{𝑋} ∧ 𝐽 ∈ ω) → (𝑎‘𝐽) = 𝑋) |
| 56 | 55 | 3ad2antr2 1190 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → (𝑎‘𝐽) = 𝑋) |
| 57 | 54, 56 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → ((𝑎‘𝐼) ∈ (𝑎‘𝐽) ↔ 𝑋 ∈ 𝑋)) |
| 58 | 52, 57 | mtbiri 327 |
. . . . . . . . . . 11
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
| 59 | 58 | ex 412 |
. . . . . . . . . 10
⊢ (𝑎:ω⟶{𝑋} → ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽))) |
| 60 | 51, 59 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ ({𝑋} ↑m ω) → ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽))) |
| 61 | 60 | impcom 407 |
. . . . . . . 8
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) ∧ 𝑎 ∈ ({𝑋} ↑m ω)) → ¬
(𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
| 62 | 61 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ∀𝑎 ∈ ({𝑋} ↑m ω) ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
| 63 | | rabeq0 4388 |
. . . . . . 7
⊢ ({𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)} = ∅ ↔ ∀𝑎 ∈ ({𝑋} ↑m ω) ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
| 64 | 62, 63 | sylibr 234 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)} = ∅) |
| 65 | 50, 64 | eqtrd 2777 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))} = ∅) |
| 66 | 35, 65 | eqtrd 2777 |
. . . 4
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ∅) |
| 67 | 66 | eqeq1d 2739 |
. . 3
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ({𝑋} ↑m ω) ↔ ∅
= ({𝑋} ↑m
ω))) |
| 68 | 23, 67 | bitrd 279 |
. 2
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋}⊧(𝐼∈𝑔𝐽) ↔ ∅ = ({𝑋} ↑m
ω))) |
| 69 | 19, 68 | mtbird 325 |
1
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽)) |