Step | Hyp | Ref
| Expression |
1 | | n0 3890 |
. . . 4
⊢ (𝑈 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑈) |
2 | | 0ss 3924 |
. . . . . . . . . . 11
⊢ ∅
⊆ 𝑥 |
3 | | gruss 9497 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ ∅ ⊆ 𝑥) → ∅ ∈ 𝑈) |
4 | 2, 3 | mp3an3 1405 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ∅ ∈ 𝑈) |
5 | | 0elon 5695 |
. . . . . . . . . 10
⊢ ∅
∈ On |
6 | 4, 5 | jctir 559 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (∅ ∈ 𝑈 ∧ ∅ ∈ On)) |
7 | | elin 3758 |
. . . . . . . . 9
⊢ (∅
∈ (𝑈 ∩ On) ↔
(∅ ∈ 𝑈 ∧
∅ ∈ On)) |
8 | 6, 7 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ∅ ∈ (𝑈 ∩ On)) |
9 | | gruina.1 |
. . . . . . . 8
⊢ 𝐴 = (𝑈 ∩ On) |
10 | 8, 9 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ∅ ∈ 𝐴) |
11 | | ne0i 3880 |
. . . . . . 7
⊢ (∅
∈ 𝐴 → 𝐴 ≠ ∅) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ≠ ∅) |
13 | 12 | expcom 450 |
. . . . 5
⊢ (𝑥 ∈ 𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅)) |
14 | 13 | exlimiv 1845 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅)) |
15 | 1, 14 | sylbi 206 |
. . 3
⊢ (𝑈 ≠ ∅ → (𝑈 ∈ Univ → 𝐴 ≠ ∅)) |
16 | 15 | impcom 445 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ≠ ∅) |
17 | | grutr 9494 |
. . . . . . . 8
⊢ (𝑈 ∈ Univ → Tr 𝑈) |
18 | | tron 5663 |
. . . . . . . 8
⊢ Tr
On |
19 | | trin 4691 |
. . . . . . . 8
⊢ ((Tr
𝑈 ∧ Tr On) → Tr
(𝑈 ∩
On)) |
20 | 17, 18, 19 | sylancl 693 |
. . . . . . 7
⊢ (𝑈 ∈ Univ → Tr (𝑈 ∩ On)) |
21 | | inss2 3796 |
. . . . . . . . 9
⊢ (𝑈 ∩ On) ⊆
On |
22 | | epweon 6875 |
. . . . . . . . 9
⊢ E We
On |
23 | | wess 5025 |
. . . . . . . . 9
⊢ ((𝑈 ∩ On) ⊆ On → ( E
We On → E We (𝑈 ∩
On))) |
24 | 21, 22, 23 | mp2 9 |
. . . . . . . 8
⊢ E We
(𝑈 ∩
On) |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝑈 ∈ Univ → E We (𝑈 ∩ On)) |
26 | | df-ord 5643 |
. . . . . . 7
⊢ (Ord
(𝑈 ∩ On) ↔ (Tr
(𝑈 ∩ On) ∧ E We
(𝑈 ∩
On))) |
27 | 20, 25, 26 | sylanbrc 695 |
. . . . . 6
⊢ (𝑈 ∈ Univ → Ord (𝑈 ∩ On)) |
28 | | inex1g 4729 |
. . . . . 6
⊢ (𝑈 ∈ Univ → (𝑈 ∩ On) ∈
V) |
29 | | elon2 5651 |
. . . . . 6
⊢ ((𝑈 ∩ On) ∈ On ↔ (Ord
(𝑈 ∩ On) ∧ (𝑈 ∩ On) ∈
V)) |
30 | 27, 28, 29 | sylanbrc 695 |
. . . . 5
⊢ (𝑈 ∈ Univ → (𝑈 ∩ On) ∈
On) |
31 | 9, 30 | syl5eqel 2692 |
. . . 4
⊢ (𝑈 ∈ Univ → 𝐴 ∈ On) |
32 | 31 | adantr 480 |
. . 3
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On) |
33 | | eloni 5650 |
. . . . . . 7
⊢ (𝐴 ∈ On → Ord 𝐴) |
34 | | ordirr 5658 |
. . . . . . 7
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴) |
36 | | elin 3758 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On)) |
37 | 36 | biimpri 217 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On)) |
38 | 37, 9 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ 𝐴) |
39 | 38 | expcom 450 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝐴)) |
40 | 35, 39 | mtod 188 |
. . . . 5
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈ 𝑈) |
41 | 32, 40 | syl 17 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬
𝐴 ∈ 𝑈) |
42 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∩ On) ⊆ 𝑈 |
43 | 9, 42 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ⊆ 𝑈 |
44 | 43 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈) |
45 | | vpwex 4775 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
𝑥 ∈ V |
46 | 45 | canth2 7998 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
𝑥 ≺ 𝒫
𝒫 𝑥 |
47 | 45 | pwex 4774 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝒫
𝒫 𝑥 ∈
V |
48 | 47 | cardid 9248 |
. . . . . . . . . . . . . . . . 17
⊢
(card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 |
49 | 48 | ensymi 7892 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
𝒫 𝑥 ≈
(card‘𝒫 𝒫 𝑥) |
50 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ On) |
51 | | grupw 9496 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝑥 ∈ 𝑈) |
52 | | grupw 9496 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝑥 ∈ 𝑈) → 𝒫 𝒫 𝑥 ∈ 𝑈) |
53 | 51, 52 | syldan 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝒫 𝑥 ∈ 𝑈) |
54 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → 𝐴 ∈ On) |
55 | | endom 7868 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 → (card‘𝒫
𝒫 𝑥) ≼
𝒫 𝒫 𝑥) |
56 | 48, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥 |
57 | | cardon 8653 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(card‘𝒫 𝒫 𝑥) ∈ On |
58 | | grudomon 9518 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 ∈ Univ ∧
(card‘𝒫 𝒫 𝑥) ∈ On ∧ (𝒫 𝒫 𝑥 ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫
𝑥)) →
(card‘𝒫 𝒫 𝑥) ∈ 𝑈) |
59 | 57, 58 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ Univ ∧ (𝒫
𝒫 𝑥 ∈ 𝑈 ∧ (card‘𝒫
𝒫 𝑥) ≼
𝒫 𝒫 𝑥))
→ (card‘𝒫 𝒫 𝑥) ∈ 𝑈) |
60 | 56, 59 | mpanr2 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → (card‘𝒫
𝒫 𝑥) ∈ 𝑈) |
61 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On) ↔ ((card‘𝒫
𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫
𝒫 𝑥) ∈
On)) |
62 | 61 | biimpri 217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) →
(card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On)) |
63 | 62, 9 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) →
(card‘𝒫 𝒫 𝑥) ∈ 𝐴) |
64 | 60, 57, 63 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → (card‘𝒫
𝒫 𝑥) ∈ 𝐴) |
65 | | onelss 5683 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On →
((card‘𝒫 𝒫 𝑥) ∈ 𝐴 → (card‘𝒫 𝒫
𝑥) ⊆ 𝐴)) |
66 | 54, 64, 65 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ 𝒫
𝒫 𝑥 ∈ 𝑈) → (card‘𝒫
𝒫 𝑥) ⊆ 𝐴) |
67 | 53, 66 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (card‘𝒫 𝒫
𝑥) ⊆ 𝐴) |
68 | | ssdomg 7887 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On →
((card‘𝒫 𝒫 𝑥) ⊆ 𝐴 → (card‘𝒫 𝒫
𝑥) ≼ 𝐴)) |
69 | 50, 67, 68 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (card‘𝒫 𝒫
𝑥) ≼ 𝐴) |
70 | | endomtr 7900 |
. . . . . . . . . . . . . . . 16
⊢
((𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫
𝑥) ∧
(card‘𝒫 𝒫 𝑥) ≼ 𝐴) → 𝒫 𝒫 𝑥 ≼ 𝐴) |
71 | 49, 69, 70 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝒫 𝑥 ≼ 𝐴) |
72 | | sdomdomtr 7978 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑥
≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥 ≼ 𝐴) → 𝒫 𝑥 ≺ 𝐴) |
73 | 46, 71, 72 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝒫 𝑥 ≺ 𝐴) |
74 | 44, 73 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → 𝒫 𝑥 ≺ 𝐴) |
75 | 74 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴) |
76 | | inawinalem 9390 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
77 | 31, 75, 76 | sylc 63 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) |
78 | 77 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) |
79 | | winainflem 9394 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴) |
80 | 16, 32, 78, 79 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ω
⊆ 𝐴) |
81 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
82 | 81 | canth2 7998 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ≺ 𝒫 𝑥 |
83 | | sdomtr 7983 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥 ≺ 𝐴) → 𝑥 ≺ 𝐴) |
84 | 82, 74, 83 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝐴) |
85 | 84 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴) |
86 | | iscard 8684 |
. . . . . . . . . . . 12
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) |
87 | 31, 85, 86 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ Univ →
(card‘𝐴) = 𝐴) |
88 | | cardlim 8681 |
. . . . . . . . . . . 12
⊢ (ω
⊆ (card‘𝐴)
↔ Lim (card‘𝐴)) |
89 | | sseq2 3590 |
. . . . . . . . . . . . 13
⊢
((card‘𝐴) =
𝐴 → (ω ⊆
(card‘𝐴) ↔
ω ⊆ 𝐴)) |
90 | | limeq 5652 |
. . . . . . . . . . . . 13
⊢
((card‘𝐴) =
𝐴 → (Lim
(card‘𝐴) ↔ Lim
𝐴)) |
91 | 89, 90 | bibi12d 334 |
. . . . . . . . . . . 12
⊢
((card‘𝐴) =
𝐴 → ((ω ⊆
(card‘𝐴) ↔ Lim
(card‘𝐴)) ↔
(ω ⊆ 𝐴 ↔
Lim 𝐴))) |
92 | 88, 91 | mpbii 222 |
. . . . . . . . . . 11
⊢
((card‘𝐴) =
𝐴 → (ω ⊆
𝐴 ↔ Lim 𝐴)) |
93 | 87, 92 | syl 17 |
. . . . . . . . . 10
⊢ (𝑈 ∈ Univ → (ω
⊆ 𝐴 ↔ Lim 𝐴)) |
94 | 93 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (ω
⊆ 𝐴 ↔ Lim 𝐴)) |
95 | 80, 94 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → Lim 𝐴) |
96 | | cflm 8955 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (cf‘𝐴) = ∩
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
97 | 32, 95, 96 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
98 | | cardon 8653 |
. . . . . . . . . . . 12
⊢
(card‘𝑦)
∈ On |
99 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On)) |
100 | 98, 99 | mpbiri 247 |
. . . . . . . . . . 11
⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
101 | 100 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → 𝑥 ∈ On) |
102 | 101 | exlimiv 1845 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → 𝑥 ∈ On) |
103 | 102 | abssi 3640 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ On |
104 | | fvex 6113 |
. . . . . . . . . 10
⊢
(cf‘𝐴) ∈
V |
105 | 97, 104 | syl6eqelr 2697 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ V) |
106 | | intex 4747 |
. . . . . . . . 9
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ≠ ∅ ↔ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ V) |
107 | 105, 106 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ≠
∅) |
108 | | onint 6887 |
. . . . . . . 8
⊢ (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
109 | 103, 107,
108 | sylancr 694 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
110 | 97, 109 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
111 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑥 = (cf‘𝐴) → (𝑥 = (card‘𝑦) ↔ (cf‘𝐴) = (card‘𝑦))) |
112 | 111 | anbi1d 737 |
. . . . . . . 8
⊢ (𝑥 = (cf‘𝐴) → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ↔ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)))) |
113 | 112 | exbidv 1837 |
. . . . . . 7
⊢ (𝑥 = (cf‘𝐴) → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)))) |
114 | 104, 113 | elab 3319 |
. . . . . 6
⊢
((cf‘𝐴) ∈
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))) |
115 | 110, 114 | sylib 207 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))) |
116 | | simp2rr 1124 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 = ∪ 𝑦) |
117 | | simp1l 1078 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑈 ∈ Univ) |
118 | | simp2rl 1123 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦 ⊆ 𝐴) |
119 | 118, 43 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦 ⊆ 𝑈) |
120 | 43 | sseli 3564 |
. . . . . . . . . . 11
⊢
((cf‘𝐴) ∈
𝐴 → (cf‘𝐴) ∈ 𝑈) |
121 | 120 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ∈ 𝑈) |
122 | | simp2l 1080 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) = (card‘𝑦)) |
123 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
124 | 123 | cardid 9248 |
. . . . . . . . . . 11
⊢
(card‘𝑦)
≈ 𝑦 |
125 | 122, 124 | syl6eqbr 4622 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ≈ 𝑦) |
126 | | gruen 9513 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑦 ⊆ 𝑈 ∧ ((cf‘𝐴) ∈ 𝑈 ∧ (cf‘𝐴) ≈ 𝑦)) → 𝑦 ∈ 𝑈) |
127 | 117, 119,
121, 125, 126 | syl112anc 1322 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦 ∈ 𝑈) |
128 | | gruuni 9501 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑦 ∈ 𝑈) → ∪ 𝑦 ∈ 𝑈) |
129 | 117, 127,
128 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑈) |
130 | 116, 129 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧
((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 ∈ 𝑈) |
131 | 130 | 3exp 1256 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(((cf‘𝐴) =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → ((cf‘𝐴) ∈ 𝐴 → 𝐴 ∈ 𝑈))) |
132 | 131 | exlimdv 1848 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → ((cf‘𝐴) ∈ 𝐴 → 𝐴 ∈ 𝑈))) |
133 | 115, 132 | mpd 15 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
((cf‘𝐴) ∈ 𝐴 → 𝐴 ∈ 𝑈)) |
134 | 41, 133 | mtod 188 |
. . 3
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬
(cf‘𝐴) ∈ 𝐴) |
135 | | cfon 8960 |
. . . . 5
⊢
(cf‘𝐴) ∈
On |
136 | | cfle 8959 |
. . . . . 6
⊢
(cf‘𝐴) ⊆
𝐴 |
137 | | onsseleq 5682 |
. . . . . 6
⊢
(((cf‘𝐴)
∈ On ∧ 𝐴 ∈
On) → ((cf‘𝐴)
⊆ 𝐴 ↔
((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))) |
138 | 136, 137 | mpbii 222 |
. . . . 5
⊢
(((cf‘𝐴)
∈ On ∧ 𝐴 ∈
On) → ((cf‘𝐴)
∈ 𝐴 ∨
(cf‘𝐴) = 𝐴)) |
139 | 135, 138 | mpan 702 |
. . . 4
⊢ (𝐴 ∈ On →
((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴)) |
140 | 139 | ord 391 |
. . 3
⊢ (𝐴 ∈ On → (¬
(cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) = 𝐴)) |
141 | 32, 134, 140 | sylc 63 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(cf‘𝐴) = 𝐴) |
142 | 75 | adantr 480 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴) |
143 | | elina 9388 |
. 2
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) |
144 | 16, 141, 142, 143 | syl3anbrc 1239 |
1
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) |