Step | Hyp | Ref
| Expression |
1 | | cardeq0 10052 |
. . . 4
⊢ (𝑇 ∈ Tarski →
((card‘𝑇) = ∅
↔ 𝑇 =
∅)) |
2 | 1 | necon3bid 2978 |
. . 3
⊢ (𝑇 ∈ Tarski →
((card‘𝑇) ≠
∅ ↔ 𝑇 ≠
∅)) |
3 | 2 | biimpar 481 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(card‘𝑇) ≠
∅) |
4 | | eqid 2738 |
. . . . . 6
⊢ (𝑧 ∈
(cf‘(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)})) ↦ (har‘(𝑤‘𝑧))) = (𝑧 ∈ (cf‘(ℵ‘∩ {𝑥
∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)})) ↦ (har‘(𝑤‘𝑧))) |
5 | 4 | pwcfsdom 10083 |
. . . . 5
⊢
(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}) ≺
((ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}) ↑m
(cf‘(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}))) |
6 | | vpwex 5244 |
. . . . . . . . . . . 12
⊢ 𝒫
𝑥 ∈ V |
7 | 6 | canth2 8720 |
. . . . . . . . . . 11
⊢ 𝒫
𝑥 ≺ 𝒫
𝒫 𝑥 |
8 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝑇 ∈ Tarski) |
9 | | cardon 9446 |
. . . . . . . . . . . . . . . . 17
⊢
(card‘𝑇)
∈ On |
10 | 9 | oneli 6280 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (card‘𝑇) → 𝑥 ∈ On) |
11 | 10 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝑥 ∈ On) |
12 | | cardsdomelir 9475 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (card‘𝑇) → 𝑥 ≺ 𝑇) |
13 | 12 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝑥 ≺ 𝑇) |
14 | | tskord 10280 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ On ∧ 𝑥 ≺ 𝑇) → 𝑥 ∈ 𝑇) |
15 | 8, 11, 13, 14 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝑥 ∈ 𝑇) |
16 | | tskpw 10253 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇) → 𝒫 𝑥 ∈ 𝑇) |
17 | | tskpwss 10252 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Tarski ∧ 𝒫
𝑥 ∈ 𝑇) → 𝒫 𝒫 𝑥 ⊆ 𝑇) |
18 | 16, 17 | syldan 594 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇) → 𝒫 𝒫 𝑥 ⊆ 𝑇) |
19 | 15, 18 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝒫 𝒫
𝑥 ⊆ 𝑇) |
20 | | ssdomg 8601 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Tarski → (𝒫
𝒫 𝑥 ⊆ 𝑇 → 𝒫 𝒫
𝑥 ≼ 𝑇)) |
21 | 8, 19, 20 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝒫 𝒫
𝑥 ≼ 𝑇) |
22 | | cardidg 10048 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ Tarski →
(card‘𝑇) ≈
𝑇) |
23 | 22 | ensymd 8606 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇)) |
24 | 23 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝑇 ≈ (card‘𝑇)) |
25 | | domentr 8614 |
. . . . . . . . . . . 12
⊢
((𝒫 𝒫 𝑥 ≼ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝒫 𝒫 𝑥 ≼ (card‘𝑇)) |
26 | 21, 24, 25 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝒫 𝒫
𝑥 ≼ (card‘𝑇)) |
27 | | sdomdomtr 8700 |
. . . . . . . . . . 11
⊢
((𝒫 𝑥
≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥 ≼ (card‘𝑇)) → 𝒫 𝑥 ≺ (card‘𝑇)) |
28 | 7, 26, 27 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ (card‘𝑇)) → 𝒫 𝑥 ≺ (card‘𝑇)) |
29 | 28 | ralrimiva 3096 |
. . . . . . . . 9
⊢ (𝑇 ∈ Tarski →
∀𝑥 ∈
(card‘𝑇)𝒫
𝑥 ≺ (card‘𝑇)) |
30 | 29 | adantr 484 |
. . . . . . . 8
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
∀𝑥 ∈
(card‘𝑇)𝒫
𝑥 ≺ (card‘𝑇)) |
31 | | inawinalem 10189 |
. . . . . . . . . 10
⊢
((card‘𝑇)
∈ On → (∀𝑥
∈ (card‘𝑇)𝒫 𝑥 ≺ (card‘𝑇) → ∀𝑥 ∈ (card‘𝑇)∃𝑦 ∈ (card‘𝑇)𝑥 ≺ 𝑦)) |
32 | 9, 31 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(card‘𝑇)𝒫
𝑥 ≺ (card‘𝑇) → ∀𝑥 ∈ (card‘𝑇)∃𝑦 ∈ (card‘𝑇)𝑥 ≺ 𝑦) |
33 | | winainflem 10193 |
. . . . . . . . . 10
⊢
(((card‘𝑇)
≠ ∅ ∧ (card‘𝑇) ∈ On ∧ ∀𝑥 ∈ (card‘𝑇)∃𝑦 ∈ (card‘𝑇)𝑥 ≺ 𝑦) → ω ⊆ (card‘𝑇)) |
34 | 9, 33 | mp3an2 1450 |
. . . . . . . . 9
⊢
(((card‘𝑇)
≠ ∅ ∧ ∀𝑥 ∈ (card‘𝑇)∃𝑦 ∈ (card‘𝑇)𝑥 ≺ 𝑦) → ω ⊆ (card‘𝑇)) |
35 | 32, 34 | sylan2 596 |
. . . . . . . 8
⊢
(((card‘𝑇)
≠ ∅ ∧ ∀𝑥 ∈ (card‘𝑇)𝒫 𝑥 ≺ (card‘𝑇)) → ω ⊆ (card‘𝑇)) |
36 | 3, 30, 35 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω
⊆ (card‘𝑇)) |
37 | | cardidm 9461 |
. . . . . . 7
⊢
(card‘(card‘𝑇)) = (card‘𝑇) |
38 | | cardaleph 9589 |
. . . . . . 7
⊢ ((ω
⊆ (card‘𝑇)
∧ (card‘(card‘𝑇)) = (card‘𝑇)) → (card‘𝑇) = (ℵ‘∩ {𝑥
∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)})) |
39 | 36, 37, 38 | sylancl 589 |
. . . . . 6
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(card‘𝑇) =
(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)})) |
40 | 39 | fveq2d 6678 |
. . . . . . 7
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(cf‘(card‘𝑇)) =
(cf‘(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}))) |
41 | 39, 40 | oveq12d 7188 |
. . . . . 6
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
((card‘𝑇)
↑m (cf‘(card‘𝑇))) = ((ℵ‘∩ {𝑥
∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}) ↑m
(cf‘(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)})))) |
42 | 39, 41 | breq12d 5043 |
. . . . 5
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
((card‘𝑇) ≺
((card‘𝑇)
↑m (cf‘(card‘𝑇))) ↔ (ℵ‘∩ {𝑥
∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}) ≺ ((ℵ‘∩ {𝑥
∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}) ↑m
(cf‘(ℵ‘∩ {𝑥 ∈ On ∣ (card‘𝑇) ⊆ (ℵ‘𝑥)}))))) |
43 | 5, 42 | mpbiri 261 |
. . . 4
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(card‘𝑇) ≺
((card‘𝑇)
↑m (cf‘(card‘𝑇)))) |
44 | | simp1 1137 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇) ∧
𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇))))
→ 𝑇 ∈
Tarski) |
45 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇) ∧
𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇))))
→ 𝑥 ∈
((card‘𝑇)
↑m (cf‘(card‘𝑇)))) |
46 | | fvex 6687 |
. . . . . . . . . . . . . . . 16
⊢
(card‘𝑇)
∈ V |
47 | | fvex 6687 |
. . . . . . . . . . . . . . . 16
⊢
(cf‘(card‘𝑇)) ∈ V |
48 | 46, 47 | elmap 8481 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
↔ 𝑥:(cf‘(card‘𝑇))⟶(card‘𝑇)) |
49 | | fssxp 6532 |
. . . . . . . . . . . . . . 15
⊢ (𝑥:(cf‘(card‘𝑇))⟶(card‘𝑇) → 𝑥 ⊆ ((cf‘(card‘𝑇)) × (card‘𝑇))) |
50 | 48, 49 | sylbi 220 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
→ 𝑥 ⊆
((cf‘(card‘𝑇))
× (card‘𝑇))) |
51 | 15 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ Tarski → (𝑥 ∈ (card‘𝑇) → 𝑥 ∈ 𝑇)) |
52 | 51 | ssrdv 3883 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ Tarski →
(card‘𝑇) ⊆
𝑇) |
53 | | cfle 9754 |
. . . . . . . . . . . . . . . . 17
⊢
(cf‘(card‘𝑇)) ⊆ (card‘𝑇) |
54 | | sstr 3885 |
. . . . . . . . . . . . . . . . 17
⊢
(((cf‘(card‘𝑇)) ⊆ (card‘𝑇) ∧ (card‘𝑇) ⊆ 𝑇) → (cf‘(card‘𝑇)) ⊆ 𝑇) |
55 | 53, 54 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢
((card‘𝑇)
⊆ 𝑇 →
(cf‘(card‘𝑇))
⊆ 𝑇) |
56 | | tskxpss 10272 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
⊆ 𝑇 ∧
(card‘𝑇) ⊆
𝑇) →
((cf‘(card‘𝑇))
× (card‘𝑇))
⊆ 𝑇) |
57 | 56 | 3exp 1120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ Tarski →
((cf‘(card‘𝑇))
⊆ 𝑇 →
((card‘𝑇) ⊆
𝑇 →
((cf‘(card‘𝑇))
× (card‘𝑇))
⊆ 𝑇))) |
58 | 57 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ Tarski →
((card‘𝑇) ⊆
𝑇 →
((cf‘(card‘𝑇))
⊆ 𝑇 →
((cf‘(card‘𝑇))
× (card‘𝑇))
⊆ 𝑇))) |
59 | 55, 58 | mpdi 45 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ Tarski →
((card‘𝑇) ⊆
𝑇 →
((cf‘(card‘𝑇))
× (card‘𝑇))
⊆ 𝑇)) |
60 | 52, 59 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ Tarski →
((cf‘(card‘𝑇))
× (card‘𝑇))
⊆ 𝑇) |
61 | | sstr2 3884 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆
((cf‘(card‘𝑇))
× (card‘𝑇))
→ (((cf‘(card‘𝑇)) × (card‘𝑇)) ⊆ 𝑇 → 𝑥 ⊆ 𝑇)) |
62 | 50, 60, 61 | syl2im 40 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
→ (𝑇 ∈ Tarski
→ 𝑥 ⊆ 𝑇)) |
63 | 45, 44, 62 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇) ∧
𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇))))
→ 𝑥 ⊆ 𝑇) |
64 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇) ∧
𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇))))
→ (cf‘(card‘𝑇)) ∈ (card‘𝑇)) |
65 | | ffn 6504 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥:(cf‘(card‘𝑇))⟶(card‘𝑇) → 𝑥 Fn (cf‘(card‘𝑇))) |
66 | | fndmeng 8634 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 Fn (cf‘(card‘𝑇)) ∧
(cf‘(card‘𝑇))
∈ V) → (cf‘(card‘𝑇)) ≈ 𝑥) |
67 | 65, 47, 66 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥:(cf‘(card‘𝑇))⟶(card‘𝑇) →
(cf‘(card‘𝑇))
≈ 𝑥) |
68 | 48, 67 | sylbi 220 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
→ (cf‘(card‘𝑇)) ≈ 𝑥) |
69 | 68 | ensymd 8606 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
→ 𝑥 ≈
(cf‘(card‘𝑇))) |
70 | | cardsdomelir 9475 |
. . . . . . . . . . . . . 14
⊢
((cf‘(card‘𝑇)) ∈ (card‘𝑇) → (cf‘(card‘𝑇)) ≺ 𝑇) |
71 | | ensdomtr 8703 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ≈
(cf‘(card‘𝑇))
∧ (cf‘(card‘𝑇)) ≺ 𝑇) → 𝑥 ≺ 𝑇) |
72 | 69, 70, 71 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
∧ (cf‘(card‘𝑇)) ∈ (card‘𝑇)) → 𝑥 ≺ 𝑇) |
73 | 45, 64, 72 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇) ∧
𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇))))
→ 𝑥 ≺ 𝑇) |
74 | | tskssel 10257 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ⊆ 𝑇 ∧ 𝑥 ≺ 𝑇) → 𝑥 ∈ 𝑇) |
75 | 44, 63, 73, 74 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇) ∧
𝑥 ∈ ((card‘𝑇) ↑m
(cf‘(card‘𝑇))))
→ 𝑥 ∈ 𝑇) |
76 | 75 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇))
→ (𝑥 ∈
((card‘𝑇)
↑m (cf‘(card‘𝑇))) → 𝑥 ∈ 𝑇)) |
77 | 76 | ssrdv 3883 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇))
→ ((card‘𝑇)
↑m (cf‘(card‘𝑇))) ⊆ 𝑇) |
78 | | ssdomg 8601 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Tarski →
(((card‘𝑇)
↑m (cf‘(card‘𝑇))) ⊆ 𝑇 → ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
≼ 𝑇)) |
79 | 78 | imp 410 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Tarski ∧
((card‘𝑇)
↑m (cf‘(card‘𝑇))) ⊆ 𝑇) → ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
≼ 𝑇) |
80 | 77, 79 | syldan 594 |
. . . . . . . 8
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇))
→ ((card‘𝑇)
↑m (cf‘(card‘𝑇))) ≼ 𝑇) |
81 | 23 | adantr 484 |
. . . . . . . 8
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇))
→ 𝑇 ≈
(card‘𝑇)) |
82 | | domentr 8614 |
. . . . . . . 8
⊢
((((card‘𝑇)
↑m (cf‘(card‘𝑇))) ≼ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))
≼ (card‘𝑇)) |
83 | 80, 81, 82 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇))
→ ((card‘𝑇)
↑m (cf‘(card‘𝑇))) ≼ (card‘𝑇)) |
84 | | domnsym 8693 |
. . . . . . 7
⊢
(((card‘𝑇)
↑m (cf‘(card‘𝑇))) ≼ (card‘𝑇) → ¬ (card‘𝑇) ≺ ((card‘𝑇) ↑m
(cf‘(card‘𝑇)))) |
85 | 83, 84 | syl 17 |
. . . . . 6
⊢ ((𝑇 ∈ Tarski ∧
(cf‘(card‘𝑇))
∈ (card‘𝑇))
→ ¬ (card‘𝑇)
≺ ((card‘𝑇)
↑m (cf‘(card‘𝑇)))) |
86 | 85 | ex 416 |
. . . . 5
⊢ (𝑇 ∈ Tarski →
((cf‘(card‘𝑇))
∈ (card‘𝑇)
→ ¬ (card‘𝑇)
≺ ((card‘𝑇)
↑m (cf‘(card‘𝑇))))) |
87 | 86 | adantr 484 |
. . . 4
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
((cf‘(card‘𝑇))
∈ (card‘𝑇)
→ ¬ (card‘𝑇)
≺ ((card‘𝑇)
↑m (cf‘(card‘𝑇))))) |
88 | 43, 87 | mt2d 138 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ¬
(cf‘(card‘𝑇))
∈ (card‘𝑇)) |
89 | | cfon 9755 |
. . . . . 6
⊢
(cf‘(card‘𝑇)) ∈ On |
90 | 89, 9 | onsseli 6287 |
. . . . 5
⊢
((cf‘(card‘𝑇)) ⊆ (card‘𝑇) ↔ ((cf‘(card‘𝑇)) ∈ (card‘𝑇) ∨
(cf‘(card‘𝑇)) =
(card‘𝑇))) |
91 | 53, 90 | mpbi 233 |
. . . 4
⊢
((cf‘(card‘𝑇)) ∈ (card‘𝑇) ∨ (cf‘(card‘𝑇)) = (card‘𝑇)) |
92 | 91 | ori 860 |
. . 3
⊢ (¬
(cf‘(card‘𝑇))
∈ (card‘𝑇)
→ (cf‘(card‘𝑇)) = (card‘𝑇)) |
93 | 88, 92 | syl 17 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(cf‘(card‘𝑇)) =
(card‘𝑇)) |
94 | | elina 10187 |
. 2
⊢
((card‘𝑇)
∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧
(cf‘(card‘𝑇)) =
(card‘𝑇) ∧
∀𝑥 ∈
(card‘𝑇)𝒫
𝑥 ≺ (card‘𝑇))) |
95 | 3, 93, 30, 94 | syl3anbrc 1344 |
1
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(card‘𝑇) ∈
Inacc) |