| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dfac10 |
⊢ ( CHOICE ↔ dom card = V ) |
| 2 |
|
vex |
⊢ 𝑐 ∈ V |
| 3 |
|
eleq2 |
⊢ ( dom card = V → ( 𝑐 ∈ dom card ↔ 𝑐 ∈ V ) ) |
| 4 |
2 3
|
mpbiri |
⊢ ( dom card = V → 𝑐 ∈ dom card ) |
| 5 |
|
infxpidm2 |
⊢ ( ( 𝑐 ∈ dom card ∧ ω ≼ 𝑐 ) → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) |
| 6 |
5
|
ex |
⊢ ( 𝑐 ∈ dom card → ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ) |
| 7 |
4 6
|
syl |
⊢ ( dom card = V → ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ) |
| 8 |
7
|
alrimiv |
⊢ ( dom card = V → ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ) |
| 9 |
|
finnum |
⊢ ( 𝑎 ∈ Fin → 𝑎 ∈ dom card ) |
| 10 |
9
|
adantl |
⊢ ( ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ∧ 𝑎 ∈ Fin ) → 𝑎 ∈ dom card ) |
| 11 |
|
harcl |
⊢ ( har ‘ 𝑎 ) ∈ On |
| 12 |
|
onenon |
⊢ ( ( har ‘ 𝑎 ) ∈ On → ( har ‘ 𝑎 ) ∈ dom card ) |
| 13 |
11 12
|
ax-mp |
⊢ ( har ‘ 𝑎 ) ∈ dom card |
| 14 |
|
fvex |
⊢ ( har ‘ 𝑎 ) ∈ V |
| 15 |
|
vex |
⊢ 𝑎 ∈ V |
| 16 |
14 15
|
unex |
⊢ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∈ V |
| 17 |
|
harinf |
⊢ ( ( 𝑎 ∈ V ∧ ¬ 𝑎 ∈ Fin ) → ω ⊆ ( har ‘ 𝑎 ) ) |
| 18 |
15 17
|
mpan |
⊢ ( ¬ 𝑎 ∈ Fin → ω ⊆ ( har ‘ 𝑎 ) ) |
| 19 |
|
ssun1 |
⊢ ( har ‘ 𝑎 ) ⊆ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) |
| 20 |
18 19
|
sstrdi |
⊢ ( ¬ 𝑎 ∈ Fin → ω ⊆ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) |
| 21 |
|
ssdomg |
⊢ ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∈ V → ( ω ⊆ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ω ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 22 |
16 20 21
|
mpsyl |
⊢ ( ¬ 𝑎 ∈ Fin → ω ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) |
| 23 |
|
breq2 |
⊢ ( 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ω ≼ 𝑐 ↔ ω ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 24 |
|
xpeq12 |
⊢ ( ( 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∧ 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) → ( 𝑐 × 𝑐 ) = ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 25 |
24
|
anidms |
⊢ ( 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( 𝑐 × 𝑐 ) = ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 26 |
|
id |
⊢ ( 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) |
| 27 |
25 26
|
breq12d |
⊢ ( 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ( 𝑐 × 𝑐 ) ≈ 𝑐 ↔ ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 28 |
23 27
|
imbi12d |
⊢ ( 𝑐 = ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ↔ ( ω ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) ) |
| 29 |
16 28
|
spcv |
⊢ ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) → ( ω ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 30 |
22 29
|
syl5 |
⊢ ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) → ( ¬ 𝑎 ∈ Fin → ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 31 |
30
|
imp |
⊢ ( ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ∧ ¬ 𝑎 ∈ Fin ) → ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) |
| 32 |
|
harndom |
⊢ ¬ ( har ‘ 𝑎 ) ≼ 𝑎 |
| 33 |
|
ssdomg |
⊢ ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∈ V → ( ( har ‘ 𝑎 ) ⊆ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( har ‘ 𝑎 ) ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ) |
| 34 |
16 19 33
|
mp2 |
⊢ ( har ‘ 𝑎 ) ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) |
| 35 |
|
domtr |
⊢ ( ( ( har ‘ 𝑎 ) ≼ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∧ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ 𝑎 ) → ( har ‘ 𝑎 ) ≼ 𝑎 ) |
| 36 |
34 35
|
mpan |
⊢ ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ 𝑎 → ( har ‘ 𝑎 ) ≼ 𝑎 ) |
| 37 |
32 36
|
mto |
⊢ ¬ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ 𝑎 |
| 38 |
|
unxpwdom2 |
⊢ ( ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ∨ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ 𝑎 ) ) |
| 39 |
|
orel2 |
⊢ ( ¬ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ 𝑎 → ( ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ∨ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ 𝑎 ) → ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ) ) |
| 40 |
37 38 39
|
mpsyl |
⊢ ( ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) × ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) ≈ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) → ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ) |
| 41 |
31 40
|
syl |
⊢ ( ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ∧ ¬ 𝑎 ∈ Fin ) → ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ) |
| 42 |
|
wdomnumr |
⊢ ( ( har ‘ 𝑎 ) ∈ dom card → ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ↔ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ ( har ‘ 𝑎 ) ) ) |
| 43 |
13 42
|
ax-mp |
⊢ ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼* ( har ‘ 𝑎 ) ↔ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ ( har ‘ 𝑎 ) ) |
| 44 |
41 43
|
sylib |
⊢ ( ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ∧ ¬ 𝑎 ∈ Fin ) → ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ ( har ‘ 𝑎 ) ) |
| 45 |
|
numdom |
⊢ ( ( ( har ‘ 𝑎 ) ∈ dom card ∧ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ≼ ( har ‘ 𝑎 ) ) → ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∈ dom card ) |
| 46 |
13 44 45
|
sylancr |
⊢ ( ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ∧ ¬ 𝑎 ∈ Fin ) → ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∈ dom card ) |
| 47 |
|
ssun2 |
⊢ 𝑎 ⊆ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) |
| 48 |
|
ssnum |
⊢ ( ( ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ∈ dom card ∧ 𝑎 ⊆ ( ( har ‘ 𝑎 ) ∪ 𝑎 ) ) → 𝑎 ∈ dom card ) |
| 49 |
46 47 48
|
sylancl |
⊢ ( ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ∧ ¬ 𝑎 ∈ Fin ) → 𝑎 ∈ dom card ) |
| 50 |
10 49
|
pm2.61dan |
⊢ ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) → 𝑎 ∈ dom card ) |
| 51 |
50
|
alrimiv |
⊢ ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) → ∀ 𝑎 𝑎 ∈ dom card ) |
| 52 |
|
eqv |
⊢ ( dom card = V ↔ ∀ 𝑎 𝑎 ∈ dom card ) |
| 53 |
51 52
|
sylibr |
⊢ ( ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) → dom card = V ) |
| 54 |
8 53
|
impbii |
⊢ ( dom card = V ↔ ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ) |
| 55 |
1 54
|
bitri |
⊢ ( CHOICE ↔ ∀ 𝑐 ( ω ≼ 𝑐 → ( 𝑐 × 𝑐 ) ≈ 𝑐 ) ) |