Step | Hyp | Ref
| Expression |
1 | | cardprclem.1 |
. . . . . . . . 9
⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥} |
2 | 1 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ (card‘𝑥) = 𝑥}) |
3 | | abid 2598 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∣ (card‘𝑥) = 𝑥} ↔ (card‘𝑥) = 𝑥) |
4 | | iscard 8684 |
. . . . . . . 8
⊢
((card‘𝑥) =
𝑥 ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 𝑦 ≺ 𝑥)) |
5 | 2, 3, 4 | 3bitri 285 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 𝑦 ≺ 𝑥)) |
6 | 5 | simplbi 475 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ On) |
7 | 6 | ssriv 3572 |
. . . . 5
⊢ 𝐴 ⊆ On |
8 | | ssonuni 6878 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ⊆ On → ∪ 𝐴
∈ On)) |
9 | 7, 8 | mpi 20 |
. . . 4
⊢ (𝐴 ∈ V → ∪ 𝐴
∈ On) |
10 | | domrefg 7876 |
. . . . 5
⊢ (∪ 𝐴
∈ On → ∪ 𝐴 ≼ ∪ 𝐴) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝐴 ∈ V → ∪ 𝐴
≼ ∪ 𝐴) |
12 | | elharval 8351 |
. . . 4
⊢ (∪ 𝐴
∈ (har‘∪ 𝐴) ↔ (∪ 𝐴 ∈ On ∧ ∪ 𝐴
≼ ∪ 𝐴)) |
13 | 9, 11, 12 | sylanbrc 695 |
. . 3
⊢ (𝐴 ∈ V → ∪ 𝐴
∈ (har‘∪ 𝐴)) |
14 | 7 | sseli 3564 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ On) |
15 | | domrefg 7876 |
. . . . . . . . . 10
⊢ (𝑧 ∈ On → 𝑧 ≼ 𝑧) |
16 | 15 | ancli 572 |
. . . . . . . . 9
⊢ (𝑧 ∈ On → (𝑧 ∈ On ∧ 𝑧 ≼ 𝑧)) |
17 | | elharval 8351 |
. . . . . . . . 9
⊢ (𝑧 ∈ (har‘𝑧) ↔ (𝑧 ∈ On ∧ 𝑧 ≼ 𝑧)) |
18 | 16, 17 | sylibr 223 |
. . . . . . . 8
⊢ (𝑧 ∈ On → 𝑧 ∈ (har‘𝑧)) |
19 | 14, 18 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (har‘𝑧)) |
20 | | harcard 8687 |
. . . . . . . 8
⊢
(card‘(har‘𝑧)) = (har‘𝑧) |
21 | | fvex 6113 |
. . . . . . . . 9
⊢
(har‘𝑧) ∈
V |
22 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = (har‘𝑧) → (card‘𝑥) = (card‘(har‘𝑧))) |
23 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (har‘𝑧) → 𝑥 = (har‘𝑧)) |
24 | 22, 23 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑥 = (har‘𝑧) → ((card‘𝑥) = 𝑥 ↔ (card‘(har‘𝑧)) = (har‘𝑧))) |
25 | 21, 24, 1 | elab2 3323 |
. . . . . . . 8
⊢
((har‘𝑧)
∈ 𝐴 ↔
(card‘(har‘𝑧))
= (har‘𝑧)) |
26 | 20, 25 | mpbir 220 |
. . . . . . 7
⊢
(har‘𝑧) ∈
𝐴 |
27 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑤 = (har‘𝑧) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (har‘𝑧))) |
28 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑤 = (har‘𝑧) → (𝑤 ∈ 𝐴 ↔ (har‘𝑧) ∈ 𝐴)) |
29 | 27, 28 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑤 = (har‘𝑧) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ↔ (𝑧 ∈ (har‘𝑧) ∧ (har‘𝑧) ∈ 𝐴))) |
30 | 21, 29 | spcev 3273 |
. . . . . . 7
⊢ ((𝑧 ∈ (har‘𝑧) ∧ (har‘𝑧) ∈ 𝐴) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴)) |
31 | 19, 26, 30 | sylancl 693 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴)) |
32 | | eluni 4375 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝐴
↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴)) |
33 | 31, 32 | sylibr 223 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴) |
34 | 33 | ssriv 3572 |
. . . 4
⊢ 𝐴 ⊆ ∪ 𝐴 |
35 | | harcard 8687 |
. . . . 5
⊢
(card‘(har‘∪ 𝐴)) = (har‘∪
𝐴) |
36 | | fvex 6113 |
. . . . . 6
⊢
(har‘∪ 𝐴) ∈ V |
37 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (har‘∪ 𝐴)
→ (card‘𝑥) =
(card‘(har‘∪ 𝐴))) |
38 | | id 22 |
. . . . . . 7
⊢ (𝑥 = (har‘∪ 𝐴)
→ 𝑥 = (har‘∪ 𝐴)) |
39 | 37, 38 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = (har‘∪ 𝐴)
→ ((card‘𝑥) =
𝑥 ↔
(card‘(har‘∪ 𝐴)) = (har‘∪
𝐴))) |
40 | 36, 39, 1 | elab2 3323 |
. . . . 5
⊢
((har‘∪ 𝐴) ∈ 𝐴 ↔ (card‘(har‘∪ 𝐴))
= (har‘∪ 𝐴)) |
41 | 35, 40 | mpbir 220 |
. . . 4
⊢
(har‘∪ 𝐴) ∈ 𝐴 |
42 | 34, 41 | sselii 3565 |
. . 3
⊢
(har‘∪ 𝐴) ∈ ∪ 𝐴 |
43 | 13, 42 | jctir 559 |
. 2
⊢ (𝐴 ∈ V → (∪ 𝐴
∈ (har‘∪ 𝐴) ∧ (har‘∪ 𝐴)
∈ ∪ 𝐴)) |
44 | | eloni 5650 |
. . 3
⊢ (∪ 𝐴
∈ On → Ord ∪ 𝐴) |
45 | | ordn2lp 5660 |
. . 3
⊢ (Ord
∪ 𝐴 → ¬ (∪
𝐴 ∈ (har‘∪ 𝐴)
∧ (har‘∪ 𝐴) ∈ ∪ 𝐴)) |
46 | 9, 44, 45 | 3syl 18 |
. 2
⊢ (𝐴 ∈ V → ¬ (∪ 𝐴
∈ (har‘∪ 𝐴) ∧ (har‘∪ 𝐴)
∈ ∪ 𝐴)) |
47 | 43, 46 | pm2.65i 184 |
1
⊢ ¬
𝐴 ∈ V |