Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . . . 6
⊢ (ω
× {𝑋}) = (ω
× {𝑋}) |
2 | | omex 9285 |
. . . . . . . 8
⊢ ω
∈ V |
3 | | snex 5340 |
. . . . . . . 8
⊢ {𝑋} ∈ V |
4 | 2, 3 | xpex 7559 |
. . . . . . 7
⊢ (ω
× {𝑋}) ∈
V |
5 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑎 = (ω × {𝑋}) → (𝑎 = (ω × {𝑋}) ↔ (ω × {𝑋}) = (ω × {𝑋}))) |
6 | 4, 5 | spcev 3535 |
. . . . . 6
⊢ ((ω
× {𝑋}) = (ω
× {𝑋}) →
∃𝑎 𝑎 = (ω × {𝑋})) |
7 | 1, 6 | mp1i 13 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ∃𝑎 𝑎 = (ω × {𝑋})) |
8 | 3, 2 | pm3.2i 474 |
. . . . . . . 8
⊢ ({𝑋} ∈ V ∧ ω ∈
V) |
9 | | elmapg 8544 |
. . . . . . . 8
⊢ (({𝑋} ∈ V ∧ ω ∈
V) → (𝑎 ∈ ({𝑋} ↑m ω)
↔ 𝑎:ω⟶{𝑋})) |
10 | 8, 9 | mp1i 13 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝑎 ∈ ({𝑋} ↑m ω) ↔ 𝑎:ω⟶{𝑋})) |
11 | | fconst2g 7039 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑎:ω⟶{𝑋} ↔ 𝑎 = (ω × {𝑋}))) |
12 | 11 | 3ad2ant3 1137 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝑎:ω⟶{𝑋} ↔ 𝑎 = (ω × {𝑋}))) |
13 | 10, 12 | bitrd 282 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝑎 ∈ ({𝑋} ↑m ω) ↔ 𝑎 = (ω × {𝑋}))) |
14 | 13 | exbidv 1929 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (∃𝑎 𝑎 ∈ ({𝑋} ↑m ω) ↔
∃𝑎 𝑎 = (ω × {𝑋}))) |
15 | 7, 14 | mpbird 260 |
. . . 4
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ∃𝑎 𝑎 ∈ ({𝑋} ↑m
ω)) |
16 | | neq0 4276 |
. . . 4
⊢ (¬
({𝑋} ↑m
ω) = ∅ ↔ ∃𝑎 𝑎 ∈ ({𝑋} ↑m
ω)) |
17 | 15, 16 | sylibr 237 |
. . 3
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ ({𝑋} ↑m ω) =
∅) |
18 | | eqcom 2746 |
. . 3
⊢ (({𝑋} ↑m ω) =
∅ ↔ ∅ = ({𝑋} ↑m
ω)) |
19 | 17, 18 | sylnib 331 |
. 2
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ ∅ = ({𝑋} ↑m
ω)) |
20 | | ovex 7267 |
. . . . 5
⊢ (𝐼∈𝑔𝐽) ∈ V |
21 | 3, 20 | pm3.2i 474 |
. . . 4
⊢ ({𝑋} ∈ V ∧ (𝐼∈𝑔𝐽) ∈ V) |
22 | | prv 33131 |
. . . 4
⊢ (({𝑋} ∈ V ∧ (𝐼∈𝑔𝐽) ∈ V) → ({𝑋}⊧(𝐼∈𝑔𝐽) ↔ ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ({𝑋} ↑m
ω))) |
23 | 21, 22 | mp1i 13 |
. . 3
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋}⊧(𝐼∈𝑔𝐽) ↔ ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ({𝑋} ↑m
ω))) |
24 | | goel 33050 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) = 〈∅, 〈𝐼, 𝐽〉〉) |
25 | | 0ex 5216 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
26 | 25 | snid 4593 |
. . . . . . . . . . 11
⊢ ∅
∈ {∅} |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → ∅
∈ {∅}) |
28 | | opelxpi 5605 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
〈𝐼, 𝐽〉 ∈ (ω ×
ω)) |
29 | 27, 28 | opelxpd 5606 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
〈∅, 〈𝐼,
𝐽〉〉 ∈
({∅} × (ω × ω))) |
30 | 24, 29 | eqeltrd 2840 |
. . . . . . . 8
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ ({∅} ×
(ω × ω))) |
31 | | fmla0xp 33086 |
. . . . . . . 8
⊢
(Fmla‘∅) = ({∅} × (ω ×
ω)) |
32 | 30, 31 | eleqtrrdi 2851 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈
(Fmla‘∅)) |
33 | 32 | 3adant3 1134 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (𝐼∈𝑔𝐽) ∈
(Fmla‘∅)) |
34 | | satefvfmla0 33121 |
. . . . . 6
⊢ (({𝑋} ∈ V ∧ (𝐼∈𝑔𝐽) ∈ (Fmla‘∅))
→ ({𝑋}
Sat∈ (𝐼∈𝑔𝐽)) = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))}) |
35 | 3, 33, 34 | sylancr 590 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))}) |
36 | 24 | fveq2d 6742 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(𝐼∈𝑔𝐽)) = (2nd ‘〈∅,
〈𝐼, 𝐽〉〉)) |
37 | | opex 5364 |
. . . . . . . . . . . . . 14
⊢
〈𝐼, 𝐽〉 ∈ V |
38 | 25, 37 | op2nd 7791 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈∅, 〈𝐼, 𝐽〉〉) = 〈𝐼, 𝐽〉 |
39 | 36, 38 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(𝐼∈𝑔𝐽)) = 〈𝐼, 𝐽〉) |
40 | 39 | fveq2d 6742 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(1st ‘(2nd ‘(𝐼∈𝑔𝐽))) = (1st ‘〈𝐼, 𝐽〉)) |
41 | | op1stg 7794 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(1st ‘〈𝐼, 𝐽〉) = 𝐼) |
42 | 40, 41 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(1st ‘(2nd ‘(𝐼∈𝑔𝐽))) = 𝐼) |
43 | 42 | fveq2d 6742 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) = (𝑎‘𝐼)) |
44 | 39 | fveq2d 6742 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(2nd ‘(𝐼∈𝑔𝐽))) = (2nd ‘〈𝐼, 𝐽〉)) |
45 | | op2ndg 7795 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘〈𝐼, 𝐽〉) = 𝐽) |
46 | 44, 45 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) →
(2nd ‘(2nd ‘(𝐼∈𝑔𝐽))) = 𝐽) |
47 | 46 | fveq2d 6742 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝑎‘(2nd
‘(2nd ‘(𝐼∈𝑔𝐽)))) = (𝑎‘𝐽)) |
48 | 43, 47 | eleq12d 2834 |
. . . . . . . 8
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → ((𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽)))) ↔ (𝑎‘𝐼) ∈ (𝑎‘𝐽))) |
49 | 48 | rabbidv 3404 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))} = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)}) |
50 | 49 | 3adant3 1134 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))} = {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)}) |
51 | | elmapi 8553 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ({𝑋} ↑m ω) → 𝑎:ω⟶{𝑋}) |
52 | | elirr 9240 |
. . . . . . . . . . . 12
⊢ ¬
𝑋 ∈ 𝑋 |
53 | | fvconst 7000 |
. . . . . . . . . . . . . 14
⊢ ((𝑎:ω⟶{𝑋} ∧ 𝐼 ∈ ω) → (𝑎‘𝐼) = 𝑋) |
54 | 53 | 3ad2antr1 1190 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → (𝑎‘𝐼) = 𝑋) |
55 | | fvconst 7000 |
. . . . . . . . . . . . . 14
⊢ ((𝑎:ω⟶{𝑋} ∧ 𝐽 ∈ ω) → (𝑎‘𝐽) = 𝑋) |
56 | 55 | 3ad2antr2 1191 |
. . . . . . . . . . . . 13
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → (𝑎‘𝐽) = 𝑋) |
57 | 54, 56 | eleq12d 2834 |
. . . . . . . . . . . 12
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → ((𝑎‘𝐼) ∈ (𝑎‘𝐽) ↔ 𝑋 ∈ 𝑋)) |
58 | 52, 57 | mtbiri 330 |
. . . . . . . . . . 11
⊢ ((𝑎:ω⟶{𝑋} ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉)) → ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
59 | 58 | ex 416 |
. . . . . . . . . 10
⊢ (𝑎:ω⟶{𝑋} → ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽))) |
60 | 51, 59 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ ({𝑋} ↑m ω) → ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽))) |
61 | 60 | impcom 411 |
. . . . . . . 8
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) ∧ 𝑎 ∈ ({𝑋} ↑m ω)) → ¬
(𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
62 | 61 | ralrimiva 3107 |
. . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ∀𝑎 ∈ ({𝑋} ↑m ω) ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
63 | | rabeq0 4315 |
. . . . . . 7
⊢ ({𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)} = ∅ ↔ ∀𝑎 ∈ ({𝑋} ↑m ω) ¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽)) |
64 | 62, 63 | sylibr 237 |
. . . . . 6
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘𝐼) ∈ (𝑎‘𝐽)} = ∅) |
65 | 50, 64 | eqtrd 2779 |
. . . . 5
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → {𝑎 ∈ ({𝑋} ↑m ω) ∣ (𝑎‘(1st
‘(2nd ‘(𝐼∈𝑔𝐽)))) ∈ (𝑎‘(2nd ‘(2nd
‘(𝐼∈𝑔𝐽))))} = ∅) |
66 | 35, 65 | eqtrd 2779 |
. . . 4
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ∅) |
67 | 66 | eqeq1d 2741 |
. . 3
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → (({𝑋} Sat∈ (𝐼∈𝑔𝐽)) = ({𝑋} ↑m ω) ↔ ∅
= ({𝑋} ↑m
ω))) |
68 | 23, 67 | bitrd 282 |
. 2
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ({𝑋}⊧(𝐼∈𝑔𝐽) ↔ ∅ = ({𝑋} ↑m
ω))) |
69 | 19, 68 | mtbird 328 |
1
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽)) |