| Step | Hyp | Ref
| Expression |
| 1 | | n0 4353 |
. . . 4
⊢ (𝑈 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑈) |
| 2 | | 0ss 4400 |
. . . . . . . . . 10
⊢ ∅
⊆ 𝑥 |
| 3 | | gruss 10836 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ ∅ ⊆ 𝑥) → ∅ ∈ 𝑈) |
| 4 | 2, 3 | mp3an3 1452 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ∅ ∈ 𝑈) |
| 5 | | 0elon 6438 |
. . . . . . . . 9
⊢ ∅
∈ On |
| 6 | | elin 3967 |
. . . . . . . . 9
⊢ (∅
∈ (𝑈 ∩ On) ↔
(∅ ∈ 𝑈 ∧
∅ ∈ On)) |
| 7 | 4, 5, 6 | sylanblrc 590 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ∅ ∈ (𝑈 ∩ On)) |
| 8 | | gruina.1 |
. . . . . . . 8
⊢ 𝐴 = (𝑈 ∩ On) |
| 9 | 7, 8 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ∅ ∈ 𝐴) |
| 10 | 9 | ne0d 4342 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ≠ ∅) |
| 11 | 10 | expcom 413 |
. . . . 5
⊢ (𝑥 ∈ 𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅)) |
| 12 | 11 | exlimiv 1930 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅)) |
| 13 | 1, 12 | sylbi 217 |
. . 3
⊢ (𝑈 ≠ ∅ → (𝑈 ∈ Univ → 𝐴 ≠ ∅)) |
| 14 | 13 | impcom 407 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ≠ ∅) |
| 15 | | grutr 10833 |
. . . . . . . 8
⊢ (𝑈 ∈ Univ → Tr 𝑈) |
| 16 | | tron 6407 |
. . . . . . . 8
⊢ Tr
On |
| 17 | | trin 5271 |
. . . . . . . 8
⊢ ((Tr
𝑈 ∧ Tr On) → Tr
(𝑈 ∩
On)) |
| 18 | 15, 16, 17 | sylancl 586 |
. . . . . . 7
⊢ (𝑈 ∈ Univ → Tr (𝑈 ∩ On)) |
| 19 | | inss2 4238 |
. . . . . . . 8
⊢ (𝑈 ∩ On) ⊆
On |
| 20 | | epweon 7795 |
. . . . . . . 8
⊢ E We
On |
| 21 | | wess 5671 |
. . . . . . . 8
⊢ ((𝑈 ∩ On) ⊆ On → ( E
We On → E We (𝑈 ∩
On))) |
| 22 | 19, 20, 21 | mp2 9 |
. . . . . . 7
⊢ E We
(𝑈 ∩
On) |
| 23 | | df-ord 6387 |
. . . . . . 7
⊢ (Ord
(𝑈 ∩ On) ↔ (Tr
(𝑈 ∩ On) ∧ E We
(𝑈 ∩
On))) |
| 24 | 18, 22, 23 | sylanblrc 590 |
. . . . . 6
⊢ (𝑈 ∈ Univ → Ord (𝑈 ∩ On)) |
| 25 | | inex1g 5319 |
. . . . . 6
⊢ (𝑈 ∈ Univ → (𝑈 ∩ On) ∈
V) |
| 26 | | elon2 6395 |
. . . . . 6
⊢ ((𝑈 ∩ On) ∈ On ↔ (Ord
(𝑈 ∩ On) ∧ (𝑈 ∩ On) ∈
V)) |
| 27 | 24, 25, 26 | sylanbrc 583 |
. . . . 5
⊢ (𝑈 ∈ Univ → (𝑈 ∩ On) ∈
On) |
| 28 | 8, 27 | eqeltrid 2845 |
. . . 4
⊢ (𝑈 ∈ Univ → 𝐴 ∈ On) |
| 29 | 28 | adantr 480 |
. . 3
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On) |
| 30 | | eloni 6394 |
. . . . . . 7
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 31 | | ordirr 6402 |
. . . . . . 7
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
| 32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴) |
| 33 | | elin 3967 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On)) |
| 34 | 33 | biimpri 228 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On)) |
| 35 | 34, 8 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ 𝐴) |
| 36 | 35 | expcom 413 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝐴)) |
| 37 | 32, 36 | mtod 198 |
. . . . 5
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈ 𝑈) |
| 38 | 29, 37 | syl 17 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬
𝐴 ∈ 𝑈) |
| 39 | | inss1 4237 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∩ On) ⊆ 𝑈 |
| 40 | 8, 39 | eqsstri 4030 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ⊆ 𝑈 |
| 41 | 40 | sseli 3979 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈) |
| 42 | | vpwex 5377 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
𝑥 ∈ V |
| 43 | 42 | canth2 9170 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
𝑥 ≺ 𝒫
𝒫 𝑥 |
| 44 | 42 | pwex 5380 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝒫
𝒫 𝑥 ∈
V |
| 45 | 44 | cardid 10587 |
. . . . . . . . . . . . . . . . 17
⊢
(card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 |
| 46 | 45 | ensymi 9044 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
𝒫 𝑥 ≈
(card‘𝒫 𝒫 𝑥) |
| 47 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ On) |
| 48 | | grupw 10835 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝑥 ∈ 𝑈) |
| 49 | | grupw 10835 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝑥 ∈ 𝑈) → 𝒫 𝒫 𝑥 ∈ 𝑈) |
| 50 | 48, 49 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝒫 𝑥 ∈ 𝑈) |
| 51 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → 𝐴 ∈ On) |
| 52 | | endom 9019 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 → (card‘𝒫
𝒫 𝑥) ≼
𝒫 𝒫 𝑥) |
| 53 | 45, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥 |
| 54 | | cardon 9984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(card‘𝒫 𝒫 𝑥) ∈ On |
| 55 | | grudomon 10857 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 ∈ Univ ∧
(card‘𝒫 𝒫 𝑥) ∈ On ∧ (𝒫 𝒫 𝑥 ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫
𝑥)) →
(card‘𝒫 𝒫 𝑥) ∈ 𝑈) |
| 56 | 54, 55 | mp3an2 1451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ Univ ∧ (𝒫
𝒫 𝑥 ∈ 𝑈 ∧ (card‘𝒫
𝒫 𝑥) ≼
𝒫 𝒫 𝑥))
→ (card‘𝒫 𝒫 𝑥) ∈ 𝑈) |
| 57 | 53, 56 | mpanr2 704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → (card‘𝒫
𝒫 𝑥) ∈ 𝑈) |
| 58 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On) ↔ ((card‘𝒫
𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫
𝒫 𝑥) ∈
On)) |
| 59 | 58 | biimpri 228 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) →
(card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On)) |
| 60 | 59, 8 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) →
(card‘𝒫 𝒫 𝑥) ∈ 𝐴) |
| 61 | 57, 54, 60 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → (card‘𝒫
𝒫 𝑥) ∈ 𝐴) |
| 62 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On →
((card‘𝒫 𝒫 𝑥) ∈ 𝐴 → (card‘𝒫 𝒫
𝑥) ⊆ 𝐴)) |
| 63 | 51, 61, 62 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → (card‘𝒫
𝒫 𝑥) ⊆ 𝐴) |
| 64 | 50, 63 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (card‘𝒫 𝒫
𝑥) ⊆ 𝐴) |
| 65 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On →
((card‘𝒫 𝒫 𝑥) ⊆ 𝐴 → (card‘𝒫 𝒫
𝑥) ≼ 𝐴)) |
| 66 | 47, 64, 65 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (card‘𝒫 𝒫
𝑥) ≼ 𝐴) |
| 67 | | endomtr 9052 |
. . . . . . . . . . . . . . . 16
⊢
((𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫
𝑥) ∧
(card‘𝒫 𝒫 𝑥) ≼ 𝐴) → 𝒫 𝒫 𝑥 ≼ 𝐴) |
| 68 | 46, 66, 67 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝒫 𝑥 ≼ 𝐴) |
| 69 | | sdomdomtr 9150 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑥
≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥 ≼ 𝐴) → 𝒫 𝑥 ≺ 𝐴) |
| 70 | 43, 68, 69 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝑥 ≺ 𝐴) |
| 71 | 41, 70 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → 𝒫 𝑥 ≺ 𝐴) |
| 72 | 71 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴) |
| 73 | | inawinalem 10729 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
| 74 | 28, 72, 73 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) |
| 75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) |
| 76 | | winainflem 10733 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴) |
| 77 | 14, 29, 75, 76 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ω
⊆ 𝐴) |
| 78 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 79 | 78 | canth2 9170 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ≺ 𝒫 𝑥 |
| 80 | | sdomtr 9155 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥 ≺ 𝐴) → 𝑥 ≺ 𝐴) |
| 81 | 79, 71, 80 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝐴) |
| 82 | 81 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴) |
| 83 | | iscard 10015 |
. . . . . . . . . . . 12
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) |
| 84 | 28, 82, 83 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ Univ →
(card‘𝐴) = 𝐴) |
| 85 | | cardlim 10012 |
. . . . . . . . . . . 12
⊢ (ω
⊆ (card‘𝐴)
↔ Lim (card‘𝐴)) |
| 86 | | sseq2 4010 |
. . . . . . . . . . . . 13
⊢
((card‘𝐴) =
𝐴 → (ω ⊆
(card‘𝐴) ↔
ω ⊆ 𝐴)) |
| 87 | | limeq 6396 |
. . . . . . . . . . . . 13
⊢
((card‘𝐴) =
𝐴 → (Lim
(card‘𝐴) ↔ Lim
𝐴)) |
| 88 | 86, 87 | bibi12d 345 |
. . . . . . . . . . . 12
⊢
((card‘𝐴) =
𝐴 → ((ω ⊆
(card‘𝐴) ↔ Lim
(card‘𝐴)) ↔
(ω ⊆ 𝐴 ↔
Lim 𝐴))) |
| 89 | 85, 88 | mpbii 233 |
. . . . . . . . . . 11
⊢
((card‘𝐴) =
𝐴 → (ω ⊆
𝐴 ↔ Lim 𝐴)) |
| 90 | 84, 89 | syl 17 |
. . . . . . . . . 10
⊢ (𝑈 ∈ Univ → (ω
⊆ 𝐴 ↔ Lim 𝐴)) |
| 91 | 90 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (ω
⊆ 𝐴 ↔ Lim 𝐴)) |
| 92 | 77, 91 | mpbid 232 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → Lim 𝐴) |
| 93 | | cflm 10290 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (cf‘𝐴) = ∩
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
| 94 | 29, 92, 93 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
| 95 | | cardon 9984 |
. . . . . . . . . . . 12
⊢
(card‘𝑦)
∈ On |
| 96 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On)) |
| 97 | 95, 96 | mpbiri 258 |
. . . . . . . . . . 11
⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
| 98 | 97 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → 𝑥 ∈ On) |
| 99 | 98 | exlimiv 1930 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → 𝑥 ∈ On) |
| 100 | 99 | abssi 4070 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ On |
| 101 | | fvex 6919 |
. . . . . . . . . 10
⊢
(cf‘𝐴) ∈
V |
| 102 | 94, 101 | eqeltrrdi 2850 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ V) |
| 103 | | intex 5344 |
. . . . . . . . 9
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ≠ ∅ ↔ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ V) |
| 104 | 102, 103 | sylibr 234 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ≠
∅) |
| 105 | | onint 7810 |
. . . . . . . 8
⊢ (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
| 106 | 100, 104,
105 | sylancr 587 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
| 107 | 94, 106 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
| 108 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑥 = (cf‘𝐴) → (𝑥 = (card‘𝑦) ↔ (cf‘𝐴) = (card‘𝑦))) |
| 109 | 108 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑥 = (cf‘𝐴) → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ↔ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)))) |
| 110 | 109 | exbidv 1921 |
. . . . . . 7
⊢ (𝑥 = (cf‘𝐴) → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)))) |
| 111 | 101, 110 | elab 3679 |
. . . . . 6
⊢
((cf‘𝐴) ∈
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))) |
| 112 | 107, 111 | sylib 218 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))) |
| 113 | | simp2rr 1244 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 = ∪ 𝑦) |
| 114 | | simp1l 1198 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑈 ∈ Univ) |
| 115 | | simp2rl 1243 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦 ⊆ 𝐴) |
| 116 | 115, 40 | sstrdi 3996 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦 ⊆ 𝑈) |
| 117 | 40 | sseli 3979 |
. . . . . . . . . . 11
⊢
((cf‘𝐴) ∈
𝐴 → (cf‘𝐴) ∈ 𝑈) |
| 118 | 117 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ∈ 𝑈) |
| 119 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) = (card‘𝑦)) |
| 120 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 121 | 120 | cardid 10587 |
. . . . . . . . . . 11
⊢
(card‘𝑦)
≈ 𝑦 |
| 122 | 119, 121 | eqbrtrdi 5182 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ≈ 𝑦) |
| 123 | | gruen 10852 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑦 ⊆ 𝑈 ∧ ((cf‘𝐴) ∈ 𝑈 ∧ (cf‘𝐴) ≈ 𝑦)) → 𝑦 ∈ 𝑈) |
| 124 | 114, 116,
118, 122, 123 | syl112anc 1376 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦 ∈ 𝑈) |
| 125 | | gruuni 10840 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑦 ∈ 𝑈) → ∪ 𝑦 ∈ 𝑈) |
| 126 | 114, 124,
125 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑈) |
| 127 | 113, 126 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 ∈ 𝑈) |
| 128 | 127 | 3exp 1120 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → ((cf‘𝐴) ∈ 𝐴 → 𝐴 ∈ 𝑈))) |
| 129 | 128 | exlimdv 1933 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → ((cf‘𝐴) ∈ 𝐴 → 𝐴 ∈ 𝑈))) |
| 130 | 112, 129 | mpd 15 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
((cf‘𝐴) ∈ 𝐴 → 𝐴 ∈ 𝑈)) |
| 131 | 38, 130 | mtod 198 |
. . 3
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬
(cf‘𝐴) ∈ 𝐴) |
| 132 | | cfon 10295 |
. . . . 5
⊢
(cf‘𝐴) ∈
On |
| 133 | | cfle 10294 |
. . . . . 6
⊢
(cf‘𝐴) ⊆
𝐴 |
| 134 | | onsseleq 6425 |
. . . . . 6
⊢
(((cf‘𝐴)
∈ On ∧ 𝐴 ∈
On) → ((cf‘𝐴)
⊆ 𝐴 ↔
((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))) |
| 135 | 133, 134 | mpbii 233 |
. . . . 5
⊢
(((cf‘𝐴)
∈ On ∧ 𝐴 ∈
On) → ((cf‘𝐴)
∈ 𝐴 ∨
(cf‘𝐴) = 𝐴)) |
| 136 | 132, 135 | mpan 690 |
. . . 4
⊢ (𝐴 ∈ On →
((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴)) |
| 137 | 136 | ord 865 |
. . 3
⊢ (𝐴 ∈ On → (¬
(cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) = 𝐴)) |
| 138 | 29, 131, 137 | sylc 65 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(cf‘𝐴) = 𝐴) |
| 139 | 72 | adantr 480 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴) |
| 140 | | elina 10727 |
. 2
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) |
| 141 | 14, 138, 139, 140 | syl3anbrc 1344 |
1
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) |