Step | Hyp | Ref
| Expression |
1 | | dfac10 9751 |
. 2
⊢
(CHOICE ↔ dom card = V) |
2 | | vex 3412 |
. . . . . 6
⊢ 𝑐 ∈ V |
3 | | eleq2 2826 |
. . . . . 6
⊢ (dom card
= V → (𝑐 ∈ dom
card ↔ 𝑐 ∈
V)) |
4 | 2, 3 | mpbiri 261 |
. . . . 5
⊢ (dom card
= V → 𝑐 ∈ dom
card) |
5 | | infxpidm2 9631 |
. . . . . 6
⊢ ((𝑐 ∈ dom card ∧ ω
≼ 𝑐) → (𝑐 × 𝑐) ≈ 𝑐) |
6 | 5 | ex 416 |
. . . . 5
⊢ (𝑐 ∈ dom card → (ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) |
7 | 4, 6 | syl 17 |
. . . 4
⊢ (dom card
= V → (ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) |
8 | 7 | alrimiv 1935 |
. . 3
⊢ (dom card
= V → ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) |
9 | | finnum 9564 |
. . . . . . 7
⊢ (𝑎 ∈ Fin → 𝑎 ∈ dom
card) |
10 | 9 | adantl 485 |
. . . . . 6
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ 𝑎 ∈ Fin) → 𝑎 ∈ dom card) |
11 | | harcl 9175 |
. . . . . . . . 9
⊢
(har‘𝑎) ∈
On |
12 | | onenon 9565 |
. . . . . . . . 9
⊢
((har‘𝑎)
∈ On → (har‘𝑎) ∈ dom card) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
⊢
(har‘𝑎) ∈
dom card |
14 | | fvex 6730 |
. . . . . . . . . . . . . 14
⊢
(har‘𝑎) ∈
V |
15 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V |
16 | 14, 15 | unex 7531 |
. . . . . . . . . . . . 13
⊢
((har‘𝑎) ∪
𝑎) ∈
V |
17 | | harinf 40559 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ V ∧ ¬ 𝑎 ∈ Fin) → ω
⊆ (har‘𝑎)) |
18 | 15, 17 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑎 ∈ Fin → ω
⊆ (har‘𝑎)) |
19 | | ssun1 4086 |
. . . . . . . . . . . . . 14
⊢
(har‘𝑎)
⊆ ((har‘𝑎)
∪ 𝑎) |
20 | 18, 19 | sstrdi 3913 |
. . . . . . . . . . . . 13
⊢ (¬
𝑎 ∈ Fin → ω
⊆ ((har‘𝑎)
∪ 𝑎)) |
21 | | ssdomg 8674 |
. . . . . . . . . . . . 13
⊢
(((har‘𝑎)
∪ 𝑎) ∈ V →
(ω ⊆ ((har‘𝑎) ∪ 𝑎) → ω ≼ ((har‘𝑎) ∪ 𝑎))) |
22 | 16, 20, 21 | mpsyl 68 |
. . . . . . . . . . . 12
⊢ (¬
𝑎 ∈ Fin → ω
≼ ((har‘𝑎)
∪ 𝑎)) |
23 | | breq2 5057 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (ω ≼ 𝑐 ↔ ω ≼ ((har‘𝑎) ∪ 𝑎))) |
24 | | xpeq12 5576 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = ((har‘𝑎) ∪ 𝑎) ∧ 𝑐 = ((har‘𝑎) ∪ 𝑎)) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎))) |
25 | 24 | anidms 570 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎))) |
26 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → 𝑐 = ((har‘𝑎) ∪ 𝑎)) |
27 | 25, 26 | breq12d 5066 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((𝑐 × 𝑐) ≈ 𝑐 ↔ (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))) |
28 | 23, 27 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ↔ (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)))) |
29 | 16, 28 | spcv 3520 |
. . . . . . . . . . . 12
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))) |
30 | 22, 29 | syl5 34 |
. . . . . . . . . . 11
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → (¬ 𝑎 ∈ Fin → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))) |
31 | 30 | imp 410 |
. . . . . . . . . 10
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)) |
32 | | harndom 9178 |
. . . . . . . . . . . 12
⊢ ¬
(har‘𝑎) ≼ 𝑎 |
33 | | ssdomg 8674 |
. . . . . . . . . . . . . 14
⊢
(((har‘𝑎)
∪ 𝑎) ∈ V →
((har‘𝑎) ⊆
((har‘𝑎) ∪ 𝑎) → (har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎))) |
34 | 16, 19, 33 | mp2 9 |
. . . . . . . . . . . . 13
⊢
(har‘𝑎)
≼ ((har‘𝑎)
∪ 𝑎) |
35 | | domtr 8681 |
. . . . . . . . . . . . 13
⊢
(((har‘𝑎)
≼ ((har‘𝑎)
∪ 𝑎) ∧
((har‘𝑎) ∪ 𝑎) ≼ 𝑎) → (har‘𝑎) ≼ 𝑎) |
36 | 34, 35 | mpan 690 |
. . . . . . . . . . . 12
⊢
(((har‘𝑎)
∪ 𝑎) ≼ 𝑎 → (har‘𝑎) ≼ 𝑎) |
37 | 32, 36 | mto 200 |
. . . . . . . . . . 11
⊢ ¬
((har‘𝑎) ∪ 𝑎) ≼ 𝑎 |
38 | | unxpwdom2 9204 |
. . . . . . . . . . 11
⊢
((((har‘𝑎)
∪ 𝑎) ×
((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎) ∨ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎)) |
39 | | orel2 891 |
. . . . . . . . . . 11
⊢ (¬
((har‘𝑎) ∪ 𝑎) ≼ 𝑎 → ((((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎) ∨ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎) → ((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎))) |
40 | 37, 38, 39 | mpsyl 68 |
. . . . . . . . . 10
⊢
((((har‘𝑎)
∪ 𝑎) ×
((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎) → ((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎)) |
41 | 31, 40 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎)) |
42 | | wdomnumr 9678 |
. . . . . . . . . 10
⊢
((har‘𝑎)
∈ dom card → (((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎) ↔ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎))) |
43 | 13, 42 | ax-mp 5 |
. . . . . . . . 9
⊢
(((har‘𝑎)
∪ 𝑎)
≼* (har‘𝑎) ↔ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) |
44 | 41, 43 | sylib 221 |
. . . . . . . 8
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) |
45 | | numdom 9652 |
. . . . . . . 8
⊢
(((har‘𝑎)
∈ dom card ∧ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) → ((har‘𝑎) ∪ 𝑎) ∈ dom card) |
46 | 13, 44, 45 | sylancr 590 |
. . . . . . 7
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ∈ dom card) |
47 | | ssun2 4087 |
. . . . . . 7
⊢ 𝑎 ⊆ ((har‘𝑎) ∪ 𝑎) |
48 | | ssnum 9653 |
. . . . . . 7
⊢
((((har‘𝑎)
∪ 𝑎) ∈ dom card
∧ 𝑎 ⊆
((har‘𝑎) ∪ 𝑎)) → 𝑎 ∈ dom card) |
49 | 46, 47, 48 | sylancl 589 |
. . . . . 6
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → 𝑎 ∈ dom card) |
50 | 10, 49 | pm2.61dan 813 |
. . . . 5
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → 𝑎 ∈ dom card) |
51 | 50 | alrimiv 1935 |
. . . 4
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → ∀𝑎 𝑎 ∈ dom card) |
52 | | eqv 3417 |
. . . 4
⊢ (dom card
= V ↔ ∀𝑎 𝑎 ∈ dom
card) |
53 | 51, 52 | sylibr 237 |
. . 3
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → dom card = V) |
54 | 8, 53 | impbii 212 |
. 2
⊢ (dom card
= V ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) |
55 | 1, 54 | bitri 278 |
1
⊢
(CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) |