Step | Hyp | Ref
| Expression |
1 | | dfac10 10078 |
. 2
β’
(CHOICE β dom card = V) |
2 | | vex 3448 |
. . . . . 6
β’ π β V |
3 | | eleq2 2823 |
. . . . . 6
β’ (dom card
= V β (π β dom
card β π β
V)) |
4 | 2, 3 | mpbiri 258 |
. . . . 5
β’ (dom card
= V β π β dom
card) |
5 | | infxpidm2 9958 |
. . . . . 6
β’ ((π β dom card β§ Ο
βΌ π) β (π Γ π) β π) |
6 | 5 | ex 414 |
. . . . 5
β’ (π β dom card β (Ο
βΌ π β (π Γ π) β π)) |
7 | 4, 6 | syl 17 |
. . . 4
β’ (dom card
= V β (Ο βΌ π β (π Γ π) β π)) |
8 | 7 | alrimiv 1931 |
. . 3
β’ (dom card
= V β βπ(Ο βΌ π β (π Γ π) β π)) |
9 | | finnum 9889 |
. . . . . . 7
β’ (π β Fin β π β dom
card) |
10 | 9 | adantl 483 |
. . . . . 6
β’
((βπ(Ο
βΌ π β (π Γ π) β π) β§ π β Fin) β π β dom card) |
11 | | harcl 9500 |
. . . . . . . . 9
β’
(harβπ) β
On |
12 | | onenon 9890 |
. . . . . . . . 9
β’
((harβπ)
β On β (harβπ) β dom card) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
β’
(harβπ) β
dom card |
14 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’
(harβπ) β
V |
15 | | vex 3448 |
. . . . . . . . . . . . . 14
β’ π β V |
16 | 14, 15 | unex 7681 |
. . . . . . . . . . . . 13
β’
((harβπ) βͺ
π) β
V |
17 | | harinf 41401 |
. . . . . . . . . . . . . . 15
β’ ((π β V β§ Β¬ π β Fin) β Ο
β (harβπ)) |
18 | 15, 17 | mpan 689 |
. . . . . . . . . . . . . 14
β’ (Β¬
π β Fin β Ο
β (harβπ)) |
19 | | ssun1 4133 |
. . . . . . . . . . . . . 14
β’
(harβπ)
β ((harβπ)
βͺ π) |
20 | 18, 19 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ (Β¬
π β Fin β Ο
β ((harβπ)
βͺ π)) |
21 | | ssdomg 8943 |
. . . . . . . . . . . . 13
β’
(((harβπ)
βͺ π) β V β
(Ο β ((harβπ) βͺ π) β Ο βΌ ((harβπ) βͺ π))) |
22 | 16, 20, 21 | mpsyl 68 |
. . . . . . . . . . . 12
β’ (Β¬
π β Fin β Ο
βΌ ((harβπ)
βͺ π)) |
23 | | breq2 5110 |
. . . . . . . . . . . . . 14
β’ (π = ((harβπ) βͺ π) β (Ο βΌ π β Ο βΌ ((harβπ) βͺ π))) |
24 | | xpeq12 5659 |
. . . . . . . . . . . . . . . 16
β’ ((π = ((harβπ) βͺ π) β§ π = ((harβπ) βͺ π)) β (π Γ π) = (((harβπ) βͺ π) Γ ((harβπ) βͺ π))) |
25 | 24 | anidms 568 |
. . . . . . . . . . . . . . 15
β’ (π = ((harβπ) βͺ π) β (π Γ π) = (((harβπ) βͺ π) Γ ((harβπ) βͺ π))) |
26 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π = ((harβπ) βͺ π) β π = ((harβπ) βͺ π)) |
27 | 25, 26 | breq12d 5119 |
. . . . . . . . . . . . . 14
β’ (π = ((harβπ) βͺ π) β ((π Γ π) β π β (((harβπ) βͺ π) Γ ((harβπ) βͺ π)) β ((harβπ) βͺ π))) |
28 | 23, 27 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = ((harβπ) βͺ π) β ((Ο βΌ π β (π Γ π) β π) β (Ο βΌ ((harβπ) βͺ π) β (((harβπ) βͺ π) Γ ((harβπ) βͺ π)) β ((harβπ) βͺ π)))) |
29 | 16, 28 | spcv 3563 |
. . . . . . . . . . . 12
β’
(βπ(Ο
βΌ π β (π Γ π) β π) β (Ο βΌ ((harβπ) βͺ π) β (((harβπ) βͺ π) Γ ((harβπ) βͺ π)) β ((harβπ) βͺ π))) |
30 | 22, 29 | syl5 34 |
. . . . . . . . . . 11
β’
(βπ(Ο
βΌ π β (π Γ π) β π) β (Β¬ π β Fin β (((harβπ) βͺ π) Γ ((harβπ) βͺ π)) β ((harβπ) βͺ π))) |
31 | 30 | imp 408 |
. . . . . . . . . 10
β’
((βπ(Ο
βΌ π β (π Γ π) β π) β§ Β¬ π β Fin) β (((harβπ) βͺ π) Γ ((harβπ) βͺ π)) β ((harβπ) βͺ π)) |
32 | | harndom 9503 |
. . . . . . . . . . . 12
β’ Β¬
(harβπ) βΌ π |
33 | | ssdomg 8943 |
. . . . . . . . . . . . . 14
β’
(((harβπ)
βͺ π) β V β
((harβπ) β
((harβπ) βͺ π) β (harβπ) βΌ ((harβπ) βͺ π))) |
34 | 16, 19, 33 | mp2 9 |
. . . . . . . . . . . . 13
β’
(harβπ)
βΌ ((harβπ)
βͺ π) |
35 | | domtr 8950 |
. . . . . . . . . . . . 13
β’
(((harβπ)
βΌ ((harβπ)
βͺ π) β§
((harβπ) βͺ π) βΌ π) β (harβπ) βΌ π) |
36 | 34, 35 | mpan 689 |
. . . . . . . . . . . 12
β’
(((harβπ)
βͺ π) βΌ π β (harβπ) βΌ π) |
37 | 32, 36 | mto 196 |
. . . . . . . . . . 11
β’ Β¬
((harβπ) βͺ π) βΌ π |
38 | | unxpwdom2 9529 |
. . . . . . . . . . 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 10005 |
. . . . . . . . . 10
β’
((harβπ)
β dom card β (((harβπ) βͺ π) βΌ* (harβπ) β ((harβπ) βͺ π) βΌ (harβπ))) |
43 | 13, 42 | ax-mp 5 |
. . . . . . . . 9
β’
(((harβπ)
βͺ π)
βΌ* (harβπ) β ((harβπ) βͺ π) βΌ (harβπ)) |
44 | 41, 43 | sylib 217 |
. . . . . . . 8
β’
((βπ(Ο
βΌ π β (π Γ π) β π) β§ Β¬ π β Fin) β ((harβπ) βͺ π) βΌ (harβπ)) |
45 | | numdom 9979 |
. . . . . . . 8
β’
(((harβπ)
β dom card β§ ((harβπ) βͺ π) βΌ (harβπ)) β ((harβπ) βͺ π) β dom card) |
46 | 13, 44, 45 | sylancr 588 |
. . . . . . 7
β’
((βπ(Ο
βΌ π β (π Γ π) β π) β§ Β¬ π β Fin) β ((harβπ) βͺ π) β dom card) |
47 | | ssun2 4134 |
. . . . . . 7
β’ π β ((harβπ) βͺ π) |
48 | | ssnum 9980 |
. . . . . . 7
β’
((((harβπ)
βͺ π) β dom card
β§ π β
((harβπ) βͺ π)) β π β dom card) |
49 | 46, 47, 48 | sylancl 587 |
. . . . . 6
β’
((βπ(Ο
βΌ π β (π Γ π) β π) β§ Β¬ π β Fin) β π β dom card) |
50 | 10, 49 | pm2.61dan 812 |
. . . . 5
β’
(βπ(Ο
βΌ π β (π Γ π) β π) β π β dom card) |
51 | 50 | alrimiv 1931 |
. . . 4
β’
(βπ(Ο
βΌ π β (π Γ π) β π) β βπ π β dom card) |
52 | | eqv 3453 |
. . . 4
β’ (dom card
= V β βπ π β dom
card) |
53 | 51, 52 | sylibr 233 |
. . 3
β’
(βπ(Ο
βΌ π β (π Γ π) β π) β dom card = V) |
54 | 8, 53 | impbii 208 |
. 2
β’ (dom card
= V β βπ(Ο βΌ π β (π Γ π) β π)) |
55 | 1, 54 | bitri 275 |
1
β’
(CHOICE β βπ(Ο βΌ π β (π Γ π) β π)) |