| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfac10 10179 | . 2
⊢
(CHOICE ↔ dom card = V) | 
| 2 |  | vex 3483 | . . . . . 6
⊢ 𝑐 ∈ V | 
| 3 |  | eleq2 2829 | . . . . . 6
⊢ (dom card
= V → (𝑐 ∈ dom
card ↔ 𝑐 ∈
V)) | 
| 4 | 2, 3 | mpbiri 258 | . . . . 5
⊢ (dom card
= V → 𝑐 ∈ dom
card) | 
| 5 |  | infxpidm2 10058 | . . . . . 6
⊢ ((𝑐 ∈ dom card ∧ ω
≼ 𝑐) → (𝑐 × 𝑐) ≈ 𝑐) | 
| 6 | 5 | ex 412 | . . . . 5
⊢ (𝑐 ∈ dom card → (ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) | 
| 7 | 4, 6 | syl 17 | . . . 4
⊢ (dom card
= V → (ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) | 
| 8 | 7 | alrimiv 1926 | . . 3
⊢ (dom card
= V → ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) | 
| 9 |  | finnum 9989 | . . . . . . 7
⊢ (𝑎 ∈ Fin → 𝑎 ∈ dom
card) | 
| 10 | 9 | adantl 481 | . . . . . 6
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ 𝑎 ∈ Fin) → 𝑎 ∈ dom card) | 
| 11 |  | harcl 9600 | . . . . . . . . 9
⊢
(har‘𝑎) ∈
On | 
| 12 |  | onenon 9990 | . . . . . . . . 9
⊢
((har‘𝑎)
∈ On → (har‘𝑎) ∈ dom card) | 
| 13 | 11, 12 | ax-mp 5 | . . . . . . . 8
⊢
(har‘𝑎) ∈
dom card | 
| 14 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢
(har‘𝑎) ∈
V | 
| 15 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V | 
| 16 | 14, 15 | unex 7765 | . . . . . . . . . . . . 13
⊢
((har‘𝑎) ∪
𝑎) ∈
V | 
| 17 |  | harinf 43051 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ V ∧ ¬ 𝑎 ∈ Fin) → ω
⊆ (har‘𝑎)) | 
| 18 | 15, 17 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (¬
𝑎 ∈ Fin → ω
⊆ (har‘𝑎)) | 
| 19 |  | ssun1 4177 | . . . . . . . . . . . . . 14
⊢
(har‘𝑎)
⊆ ((har‘𝑎)
∪ 𝑎) | 
| 20 | 18, 19 | sstrdi 3995 | . . . . . . . . . . . . 13
⊢ (¬
𝑎 ∈ Fin → ω
⊆ ((har‘𝑎)
∪ 𝑎)) | 
| 21 |  | ssdomg 9041 | . . . . . . . . . . . . 13
⊢
(((har‘𝑎)
∪ 𝑎) ∈ V →
(ω ⊆ ((har‘𝑎) ∪ 𝑎) → ω ≼ ((har‘𝑎) ∪ 𝑎))) | 
| 22 | 16, 20, 21 | mpsyl 68 | . . . . . . . . . . . 12
⊢ (¬
𝑎 ∈ Fin → ω
≼ ((har‘𝑎)
∪ 𝑎)) | 
| 23 |  | breq2 5146 | . . . . . . . . . . . . . 14
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (ω ≼ 𝑐 ↔ ω ≼ ((har‘𝑎) ∪ 𝑎))) | 
| 24 |  | xpeq12 5709 | . . . . . . . . . . . . . . . 16
⊢ ((𝑐 = ((har‘𝑎) ∪ 𝑎) ∧ 𝑐 = ((har‘𝑎) ∪ 𝑎)) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎))) | 
| 25 | 24 | anidms 566 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎))) | 
| 26 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → 𝑐 = ((har‘𝑎) ∪ 𝑎)) | 
| 27 | 25, 26 | breq12d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((𝑐 × 𝑐) ≈ 𝑐 ↔ (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))) | 
| 28 | 23, 27 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ↔ (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)))) | 
| 29 | 16, 28 | spcv 3604 | . . . . . . . . . . . 12
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))) | 
| 30 | 22, 29 | syl5 34 | . . . . . . . . . . 11
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → (¬ 𝑎 ∈ Fin → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))) | 
| 31 | 30 | imp 406 | . . . . . . . . . 10
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)) | 
| 32 |  | harndom 9603 | . . . . . . . . . . . 12
⊢  ¬
(har‘𝑎) ≼ 𝑎 | 
| 33 |  | ssdomg 9041 | . . . . . . . . . . . . . 14
⊢
(((har‘𝑎)
∪ 𝑎) ∈ V →
((har‘𝑎) ⊆
((har‘𝑎) ∪ 𝑎) → (har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎))) | 
| 34 | 16, 19, 33 | mp2 9 | . . . . . . . . . . . . 13
⊢
(har‘𝑎)
≼ ((har‘𝑎)
∪ 𝑎) | 
| 35 |  | domtr 9048 | . . . . . . . . . . . . 13
⊢
(((har‘𝑎)
≼ ((har‘𝑎)
∪ 𝑎) ∧
((har‘𝑎) ∪ 𝑎) ≼ 𝑎) → (har‘𝑎) ≼ 𝑎) | 
| 36 | 34, 35 | mpan 690 | . . . . . . . . . . . 12
⊢
(((har‘𝑎)
∪ 𝑎) ≼ 𝑎 → (har‘𝑎) ≼ 𝑎) | 
| 37 | 32, 36 | mto 197 | . . . . . . . . . . 11
⊢  ¬
((har‘𝑎) ∪ 𝑎) ≼ 𝑎 | 
| 38 |  | unxpwdom2 9629 | . . . . . . . . . . 11
⊢
((((har‘𝑎)
∪ 𝑎) ×
((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎) ∨ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎)) | 
| 39 |  | orel2 890 | . . . . . . . . . . 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 10105 | . . . . . . . . . 10
⊢
((har‘𝑎)
∈ dom card → (((har‘𝑎) ∪ 𝑎) ≼* (har‘𝑎) ↔ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎))) | 
| 43 | 13, 42 | ax-mp 5 | . . . . . . . . 9
⊢
(((har‘𝑎)
∪ 𝑎)
≼* (har‘𝑎) ↔ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) | 
| 44 | 41, 43 | sylib 218 | . . . . . . . 8
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) | 
| 45 |  | numdom 10079 | . . . . . . . 8
⊢
(((har‘𝑎)
∈ dom card ∧ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) → ((har‘𝑎) ∪ 𝑎) ∈ dom card) | 
| 46 | 13, 44, 45 | sylancr 587 | . . . . . . 7
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ∈ dom card) | 
| 47 |  | ssun2 4178 | . . . . . . 7
⊢ 𝑎 ⊆ ((har‘𝑎) ∪ 𝑎) | 
| 48 |  | ssnum 10080 | . . . . . . 7
⊢
((((har‘𝑎)
∪ 𝑎) ∈ dom card
∧ 𝑎 ⊆
((har‘𝑎) ∪ 𝑎)) → 𝑎 ∈ dom card) | 
| 49 | 46, 47, 48 | sylancl 586 | . . . . . 6
⊢
((∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → 𝑎 ∈ dom card) | 
| 50 | 10, 49 | pm2.61dan 812 | . . . . 5
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → 𝑎 ∈ dom card) | 
| 51 | 50 | alrimiv 1926 | . . . 4
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → ∀𝑎 𝑎 ∈ dom card) | 
| 52 |  | eqv 3489 | . . . 4
⊢ (dom card
= V ↔ ∀𝑎 𝑎 ∈ dom
card) | 
| 53 | 51, 52 | sylibr 234 | . . 3
⊢
(∀𝑐(ω
≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → dom card = V) | 
| 54 | 8, 53 | impbii 209 | . 2
⊢ (dom card
= V ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) | 
| 55 | 1, 54 | bitri 275 | 1
⊢
(CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) |