Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . . . . . . 9
โข (๐ต โm
(โตโ๐ด)) โ
V |
2 | 1 | cardid 10488 |
. . . . . . . 8
โข
(cardโ(๐ต
โm (โตโ๐ด))) โ (๐ต โm (โตโ๐ด)) |
3 | 2 | ensymi 8947 |
. . . . . . 7
โข (๐ต โm
(โตโ๐ด)) โ
(cardโ(๐ต
โm (โตโ๐ด))) |
4 | | fvex 6856 |
. . . . . . . . . . . . . 14
โข
(โตโ๐ด)
โ V |
5 | 4 | canth2 9077 |
. . . . . . . . . . . . 13
โข
(โตโ๐ด)
โบ ๐ซ (โตโ๐ด) |
6 | 4 | pw2en 9026 |
. . . . . . . . . . . . 13
โข ๐ซ
(โตโ๐ด) โ
(2o โm (โตโ๐ด)) |
7 | | sdomentr 9058 |
. . . . . . . . . . . . 13
โข
(((โตโ๐ด)
โบ ๐ซ (โตโ๐ด) โง ๐ซ (โตโ๐ด) โ (2o
โm (โตโ๐ด))) โ (โตโ๐ด) โบ (2o โm
(โตโ๐ด))) |
8 | 5, 6, 7 | mp2an 691 |
. . . . . . . . . . . 12
โข
(โตโ๐ด)
โบ (2o โm (โตโ๐ด)) |
9 | | mapdom1 9089 |
. . . . . . . . . . . 12
โข
(2o โผ ๐ต โ (2o โm
(โตโ๐ด)) โผ
(๐ต โm
(โตโ๐ด))) |
10 | | sdomdomtr 9057 |
. . . . . . . . . . . 12
โข
(((โตโ๐ด)
โบ (2o โm (โตโ๐ด)) โง (2o โm
(โตโ๐ด)) โผ
(๐ต โm
(โตโ๐ด))) โ
(โตโ๐ด) โบ
(๐ต โm
(โตโ๐ด))) |
11 | 8, 9, 10 | sylancr 588 |
. . . . . . . . . . 11
โข
(2o โผ ๐ต โ (โตโ๐ด) โบ (๐ต โm (โตโ๐ด))) |
12 | | ficard 10506 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โm
(โตโ๐ด)) โ V
โ ((๐ต
โm (โตโ๐ด)) โ Fin โ (cardโ(๐ต โm
(โตโ๐ด))) โ
ฯ)) |
13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โm
(โตโ๐ด)) โ
Fin โ (cardโ(๐ต
โm (โตโ๐ด))) โ ฯ) |
14 | | fict 9594 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โm
(โตโ๐ด)) โ
Fin โ (๐ต
โm (โตโ๐ด)) โผ ฯ) |
15 | 13, 14 | sylbir 234 |
. . . . . . . . . . . . . . 15
โข
((cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โ (๐ต โm (โตโ๐ด)) โผ
ฯ) |
16 | | alephgeom 10023 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ On โ ฯ
โ (โตโ๐ด)) |
17 | | alephon 10010 |
. . . . . . . . . . . . . . . . 17
โข
(โตโ๐ด)
โ On |
18 | | ssdomg 8943 |
. . . . . . . . . . . . . . . . 17
โข
((โตโ๐ด)
โ On โ (ฯ โ (โตโ๐ด) โ ฯ โผ
(โตโ๐ด))) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข (ฯ
โ (โตโ๐ด)
โ ฯ โผ (โตโ๐ด)) |
20 | 16, 19 | sylbi 216 |
. . . . . . . . . . . . . . 15
โข (๐ด โ On โ ฯ
โผ (โตโ๐ด)) |
21 | | domtr 8950 |
. . . . . . . . . . . . . . 15
โข (((๐ต โm
(โตโ๐ด)) โผ
ฯ โง ฯ โผ (โตโ๐ด)) โ (๐ต โm (โตโ๐ด)) โผ (โตโ๐ด)) |
22 | 15, 20, 21 | syl2an 597 |
. . . . . . . . . . . . . 14
โข
(((cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โง ๐ด โ On) โ (๐ต โm (โตโ๐ด)) โผ (โตโ๐ด)) |
23 | | domnsym 9046 |
. . . . . . . . . . . . . 14
โข ((๐ต โm
(โตโ๐ด)) โผ
(โตโ๐ด) โ
ยฌ (โตโ๐ด)
โบ (๐ต
โm (โตโ๐ด))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
โข
(((cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โง ๐ด โ On) โ ยฌ
(โตโ๐ด) โบ
(๐ต โm
(โตโ๐ด))) |
25 | 24 | expcom 415 |
. . . . . . . . . . . 12
โข (๐ด โ On โ
((cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โ ยฌ
(โตโ๐ด) โบ
(๐ต โm
(โตโ๐ด)))) |
26 | 25 | con2d 134 |
. . . . . . . . . . 11
โข (๐ด โ On โ
((โตโ๐ด) โบ
(๐ต โm
(โตโ๐ด)) โ
ยฌ (cardโ(๐ต
โm (โตโ๐ด))) โ ฯ)) |
27 | | cardidm 9900 |
. . . . . . . . . . . 12
โข
(cardโ(cardโ(๐ต โm (โตโ๐ด)))) = (cardโ(๐ต โm
(โตโ๐ด))) |
28 | | iscard3 10034 |
. . . . . . . . . . . . 13
โข
((cardโ(cardโ(๐ต โm (โตโ๐ด)))) = (cardโ(๐ต โm
(โตโ๐ด))) โ
(cardโ(๐ต
โm (โตโ๐ด))) โ (ฯ โช ran
โต)) |
29 | | elun 4109 |
. . . . . . . . . . . . 13
โข
((cardโ(๐ต
โm (โตโ๐ด))) โ (ฯ โช ran โต)
โ ((cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โจ (cardโ(๐ต โm
(โตโ๐ด))) โ
ran โต)) |
30 | | df-or 847 |
. . . . . . . . . . . . 13
โข
(((cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โจ (cardโ(๐ต โm
(โตโ๐ด))) โ
ran โต) โ (ยฌ (cardโ(๐ต โm (โตโ๐ด))) โ ฯ โ
(cardโ(๐ต
โm (โตโ๐ด))) โ ran โต)) |
31 | 28, 29, 30 | 3bitri 297 |
. . . . . . . . . . . 12
โข
((cardโ(cardโ(๐ต โm (โตโ๐ด)))) = (cardโ(๐ต โm
(โตโ๐ด))) โ
(ยฌ (cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โ (cardโ(๐ต โm
(โตโ๐ด))) โ
ran โต)) |
32 | 27, 31 | mpbi 229 |
. . . . . . . . . . 11
โข (ยฌ
(cardโ(๐ต
โm (โตโ๐ด))) โ ฯ โ (cardโ(๐ต โm
(โตโ๐ด))) โ
ran โต) |
33 | 11, 26, 32 | syl56 36 |
. . . . . . . . . 10
โข (๐ด โ On โ (2o
โผ ๐ต โ
(cardโ(๐ต
โm (โตโ๐ด))) โ ran โต)) |
34 | | alephfnon 10006 |
. . . . . . . . . . 11
โข โต
Fn On |
35 | | fvelrnb 6904 |
. . . . . . . . . . 11
โข (โต
Fn On โ ((cardโ(๐ต โm (โตโ๐ด))) โ ran โต โ
โ๐ฅ โ On
(โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))))) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
โข
((cardโ(๐ต
โm (โตโ๐ด))) โ ran โต โ โ๐ฅ โ On (โตโ๐ฅ) = (cardโ(๐ต โm
(โตโ๐ด)))) |
37 | 33, 36 | syl6ib 251 |
. . . . . . . . 9
โข (๐ด โ On โ (2o
โผ ๐ต โ
โ๐ฅ โ On
(โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))))) |
38 | | eqid 2733 |
. . . . . . . . . . . 12
โข (๐ฆ โ
(cfโ(โตโ๐ฅ)) โฆ (harโ(๐งโ๐ฆ))) = (๐ฆ โ (cfโ(โตโ๐ฅ)) โฆ (harโ(๐งโ๐ฆ))) |
39 | 38 | pwcfsdom 10524 |
. . . . . . . . . . 11
โข
(โตโ๐ฅ)
โบ ((โตโ๐ฅ)
โm (cfโ(โตโ๐ฅ))) |
40 | | id 22 |
. . . . . . . . . . . 12
โข
((โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))) โ (โตโ๐ฅ) = (cardโ(๐ต โm (โตโ๐ด)))) |
41 | | fveq2 6843 |
. . . . . . . . . . . . 13
โข
((โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))) โ (cfโ(โตโ๐ฅ)) =
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) |
42 | 40, 41 | oveq12d 7376 |
. . . . . . . . . . . 12
โข
((โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))) โ ((โตโ๐ฅ) โm
(cfโ(โตโ๐ฅ))) = ((cardโ(๐ต โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
43 | 40, 42 | breq12d 5119 |
. . . . . . . . . . 11
โข
((โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))) โ ((โตโ๐ฅ) โบ ((โตโ๐ฅ) โm
(cfโ(โตโ๐ฅ))) โ (cardโ(๐ต โm (โตโ๐ด))) โบ ((cardโ(๐ต โm
(โตโ๐ด)))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด))))))) |
44 | 39, 43 | mpbii 232 |
. . . . . . . . . 10
โข
((โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))) โ (cardโ(๐ต โm (โตโ๐ด))) โบ ((cardโ(๐ต โm
(โตโ๐ด)))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด)))))) |
45 | 44 | rexlimivw 3145 |
. . . . . . . . 9
โข
(โ๐ฅ โ On
(โตโ๐ฅ) =
(cardโ(๐ต
โm (โตโ๐ด))) โ (cardโ(๐ต โm (โตโ๐ด))) โบ ((cardโ(๐ต โm
(โตโ๐ด)))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด)))))) |
46 | 37, 45 | syl6 35 |
. . . . . . . 8
โข (๐ด โ On โ (2o
โผ ๐ต โ
(cardโ(๐ต
โm (โตโ๐ด))) โบ ((cardโ(๐ต โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) |
47 | 46 | imp 408 |
. . . . . . 7
โข ((๐ด โ On โง 2o
โผ ๐ต) โ
(cardโ(๐ต
โm (โตโ๐ด))) โบ ((cardโ(๐ต โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
48 | | ensdomtr 9060 |
. . . . . . 7
โข (((๐ต โm
(โตโ๐ด)) โ
(cardโ(๐ต
โm (โตโ๐ด))) โง (cardโ(๐ต โm (โตโ๐ด))) โบ ((cardโ(๐ต โm
(โตโ๐ด)))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด)))))) โ (๐ต โm (โตโ๐ด)) โบ ((cardโ(๐ต โm
(โตโ๐ด)))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด)))))) |
49 | 3, 47, 48 | sylancr 588 |
. . . . . 6
โข ((๐ด โ On โง 2o
โผ ๐ต) โ (๐ต โm
(โตโ๐ด)) โบ
((cardโ(๐ต
โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
50 | | fvex 6856 |
. . . . . . . . 9
โข
(cfโ(cardโ(๐ต โm (โตโ๐ด)))) โ V |
51 | 50 | enref 8928 |
. . . . . . . 8
โข
(cfโ(cardโ(๐ต โm (โตโ๐ด)))) โ
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))) |
52 | | mapen 9088 |
. . . . . . . 8
โข
(((cardโ(๐ต
โm (โตโ๐ด))) โ (๐ต โm (โตโ๐ด)) โง
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))) โ (cfโ(cardโ(๐ต โm
(โตโ๐ด)))))
โ ((cardโ(๐ต
โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โ ((๐ต โm (โตโ๐ด)) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
53 | 2, 51, 52 | mp2an 691 |
. . . . . . 7
โข
((cardโ(๐ต
โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โ ((๐ต โm (โตโ๐ด)) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) |
54 | | cfpwsdom.1 |
. . . . . . . 8
โข ๐ต โ V |
55 | | mapxpen 9090 |
. . . . . . . 8
โข ((๐ต โ V โง
(โตโ๐ด) โ On
โง (cfโ(cardโ(๐ต โm (โตโ๐ด)))) โ V) โ ((๐ต โm
(โตโ๐ด))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด))))) โ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) |
56 | 54, 17, 50, 55 | mp3an 1462 |
. . . . . . 7
โข ((๐ต โm
(โตโ๐ด))
โm (cfโ(cardโ(๐ต โm (โตโ๐ด))))) โ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
57 | 53, 56 | entri 8951 |
. . . . . 6
โข
((cardโ(๐ต
โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
58 | | sdomentr 9058 |
. . . . . 6
โข (((๐ต โm
(โตโ๐ด)) โบ
((cardโ(๐ต
โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โง ((cardโ(๐ต โm (โตโ๐ด))) โm
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) โ (๐ต โm (โตโ๐ด)) โบ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) |
59 | 49, 57, 58 | sylancl 587 |
. . . . 5
โข ((๐ด โ On โง 2o
โผ ๐ต) โ (๐ต โm
(โตโ๐ด)) โบ
(๐ต โm
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) |
60 | 4 | xpdom2 9014 |
. . . . . . . . . 10
โข
((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โ
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โผ ((โตโ๐ด) ร (โตโ๐ด))) |
61 | 16 | biimpi 215 |
. . . . . . . . . . 11
โข (๐ด โ On โ ฯ
โ (โตโ๐ด)) |
62 | | infxpen 9955 |
. . . . . . . . . . 11
โข
(((โตโ๐ด)
โ On โง ฯ โ (โตโ๐ด)) โ ((โตโ๐ด) ร (โตโ๐ด)) โ (โตโ๐ด)) |
63 | 17, 61, 62 | sylancr 588 |
. . . . . . . . . 10
โข (๐ด โ On โ
((โตโ๐ด) ร
(โตโ๐ด)) โ
(โตโ๐ด)) |
64 | | domentr 8956 |
. . . . . . . . . 10
โข
((((โตโ๐ด)
ร (cfโ(cardโ(๐ต โm (โตโ๐ด))))) โผ
((โตโ๐ด) ร
(โตโ๐ด)) โง
((โตโ๐ด) ร
(โตโ๐ด)) โ
(โตโ๐ด)) โ
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โผ (โตโ๐ด)) |
65 | 60, 63, 64 | syl2an 597 |
. . . . . . . . 9
โข
(((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โง
๐ด โ On) โ
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) โผ (โตโ๐ด)) |
66 | | nsuceq0 6401 |
. . . . . . . . . . 11
โข suc
1o โ โ
|
67 | | dom0 9049 |
. . . . . . . . . . 11
โข (suc
1o โผ โ
โ suc 1o =
โ
) |
68 | 66, 67 | nemtbir 3037 |
. . . . . . . . . 10
โข ยฌ
suc 1o โผ โ
|
69 | | df-2o 8414 |
. . . . . . . . . . . . . 14
โข
2o = suc 1o |
70 | 69 | breq1i 5113 |
. . . . . . . . . . . . 13
โข
(2o โผ ๐ต โ suc 1o โผ ๐ต) |
71 | | breq2 5110 |
. . . . . . . . . . . . 13
โข (๐ต = โ
โ (suc
1o โผ ๐ต
โ suc 1o โผ โ
)) |
72 | 70, 71 | bitrid 283 |
. . . . . . . . . . . 12
โข (๐ต = โ
โ (2o
โผ ๐ต โ suc
1o โผ โ
)) |
73 | 72 | biimpcd 249 |
. . . . . . . . . . 11
โข
(2o โผ ๐ต โ (๐ต = โ
โ suc 1o โผ
โ
)) |
74 | 73 | adantld 492 |
. . . . . . . . . 10
โข
(2o โผ ๐ต โ ((((โตโ๐ด) ร (cfโ(cardโ(๐ต โm
(โตโ๐ด))))) =
โ
โง ๐ต = โ
)
โ suc 1o โผ โ
)) |
75 | 68, 74 | mtoi 198 |
. . . . . . . . 9
โข
(2o โผ ๐ต โ ยฌ (((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) = โ
โง ๐ต = โ
)) |
76 | | mapdom2 9095 |
. . . . . . . . 9
โข
((((โตโ๐ด)
ร (cfโ(cardโ(๐ต โm (โตโ๐ด))))) โผ
(โตโ๐ด) โง
ยฌ (((โตโ๐ด)
ร (cfโ(cardโ(๐ต โm (โตโ๐ด))))) = โ
โง ๐ต = โ
)) โ (๐ต โm
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) โผ (๐ต โm (โตโ๐ด))) |
77 | 65, 75, 76 | syl2an 597 |
. . . . . . . 8
โข
((((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โง
๐ด โ On) โง
2o โผ ๐ต)
โ (๐ต
โm ((โตโ๐ด) ร (cfโ(cardโ(๐ต โm
(โตโ๐ด))))))
โผ (๐ต
โm (โตโ๐ด))) |
78 | | domnsym 9046 |
. . . . . . . 8
โข ((๐ต โm
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) โผ (๐ต โm (โตโ๐ด)) โ ยฌ (๐ต โm
(โตโ๐ด)) โบ
(๐ต โm
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
โข
((((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โง
๐ด โ On) โง
2o โผ ๐ต)
โ ยฌ (๐ต
โm (โตโ๐ด)) โบ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))))) |
80 | 79 | expl 459 |
. . . . . 6
โข
((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โ
((๐ด โ On โง
2o โผ ๐ต)
โ ยฌ (๐ต
โm (โตโ๐ด)) โบ (๐ต โm ((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))))) |
81 | 80 | com12 32 |
. . . . 5
โข ((๐ด โ On โง 2o
โผ ๐ต) โ
((cfโ(cardโ(๐ต
โm (โตโ๐ด)))) โผ (โตโ๐ด) โ ยฌ (๐ต โm
(โตโ๐ด)) โบ
(๐ต โm
((โตโ๐ด) ร
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))))) |
82 | 59, 81 | mt2d 136 |
. . . 4
โข ((๐ด โ On โง 2o
โผ ๐ต) โ ยฌ
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))) โผ (โตโ๐ด)) |
83 | | domtri 10497 |
. . . . . 6
โข
(((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โ V โง
(โตโ๐ด) โ V)
โ ((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โ
ยฌ (โตโ๐ด)
โบ (cfโ(cardโ(๐ต โm (โตโ๐ด)))))) |
84 | 50, 4, 83 | mp2an 691 |
. . . . 5
โข
((cfโ(cardโ(๐ต โm (โตโ๐ด)))) โผ
(โตโ๐ด) โ
ยฌ (โตโ๐ด)
โบ (cfโ(cardโ(๐ต โm (โตโ๐ด))))) |
85 | 84 | biimpri 227 |
. . . 4
โข (ยฌ
(โตโ๐ด) โบ
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))) โ (cfโ(cardโ(๐ต โm
(โตโ๐ด))))
โผ (โตโ๐ด)) |
86 | 82, 85 | nsyl2 141 |
. . 3
โข ((๐ด โ On โง 2o
โผ ๐ต) โ
(โตโ๐ด) โบ
(cfโ(cardโ(๐ต
โm (โตโ๐ด))))) |
87 | 86 | ex 414 |
. 2
โข (๐ด โ On โ (2o
โผ ๐ต โ
(โตโ๐ด) โบ
(cfโ(cardโ(๐ต
โm (โตโ๐ด)))))) |
88 | | fndm 6606 |
. . . . . 6
โข (โต
Fn On โ dom โต = On) |
89 | 34, 88 | ax-mp 5 |
. . . . 5
โข dom
โต = On |
90 | 89 | eleq2i 2826 |
. . . 4
โข (๐ด โ dom โต โ ๐ด โ On) |
91 | | ndmfv 6878 |
. . . 4
โข (ยฌ
๐ด โ dom โต โ
(โตโ๐ด) =
โ
) |
92 | 90, 91 | sylnbir 331 |
. . 3
โข (ยฌ
๐ด โ On โ
(โตโ๐ด) =
โ
) |
93 | | 1n0 8435 |
. . . . . 6
โข
1o โ โ
|
94 | | 1oex 8423 |
. . . . . . 7
โข
1o โ V |
95 | 94 | 0sdom 9054 |
. . . . . 6
โข (โ
โบ 1o โ 1o โ โ
) |
96 | 93, 95 | mpbir 230 |
. . . . 5
โข โ
โบ 1o |
97 | | id 22 |
. . . . . 6
โข
((โตโ๐ด) =
โ
โ (โตโ๐ด) = โ
) |
98 | | oveq2 7366 |
. . . . . . . . . . 11
โข
((โตโ๐ด) =
โ
โ (๐ต
โm (โตโ๐ด)) = (๐ต โm
โ
)) |
99 | | map0e 8823 |
. . . . . . . . . . . 12
โข (๐ต โ V โ (๐ต โm โ
) =
1o) |
100 | 54, 99 | ax-mp 5 |
. . . . . . . . . . 11
โข (๐ต โm โ
) =
1o |
101 | 98, 100 | eqtrdi 2789 |
. . . . . . . . . 10
โข
((โตโ๐ด) =
โ
โ (๐ต
โm (โตโ๐ด)) = 1o) |
102 | 101 | fveq2d 6847 |
. . . . . . . . 9
โข
((โตโ๐ด) =
โ
โ (cardโ(๐ต โm (โตโ๐ด))) =
(cardโ1o)) |
103 | | 1onn 8587 |
. . . . . . . . . 10
โข
1o โ ฯ |
104 | | cardnn 9904 |
. . . . . . . . . 10
โข
(1o โ ฯ โ (cardโ1o) =
1o) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . 9
โข
(cardโ1o) = 1o |
106 | 102, 105 | eqtrdi 2789 |
. . . . . . . 8
โข
((โตโ๐ด) =
โ
โ (cardโ(๐ต โm (โตโ๐ด))) =
1o) |
107 | 106 | fveq2d 6847 |
. . . . . . 7
โข
((โตโ๐ด) =
โ
โ (cfโ(cardโ(๐ต โm (โตโ๐ด)))) =
(cfโ1o)) |
108 | | df-1o 8413 |
. . . . . . . . 9
โข
1o = suc โ
|
109 | 108 | fveq2i 6846 |
. . . . . . . 8
โข
(cfโ1o) = (cfโsuc โ
) |
110 | | 0elon 6372 |
. . . . . . . . 9
โข โ
โ On |
111 | | cfsuc 10198 |
. . . . . . . . 9
โข (โ
โ On โ (cfโsuc โ
) = 1o) |
112 | 110, 111 | ax-mp 5 |
. . . . . . . 8
โข
(cfโsuc โ
) = 1o |
113 | 109, 112 | eqtri 2761 |
. . . . . . 7
โข
(cfโ1o) = 1o |
114 | 107, 113 | eqtrdi 2789 |
. . . . . 6
โข
((โตโ๐ด) =
โ
โ (cfโ(cardโ(๐ต โm (โตโ๐ด)))) =
1o) |
115 | 97, 114 | breq12d 5119 |
. . . . 5
โข
((โตโ๐ด) =
โ
โ ((โตโ๐ด) โบ (cfโ(cardโ(๐ต โm
(โตโ๐ด)))) โ
โ
โบ 1o)) |
116 | 96, 115 | mpbiri 258 |
. . . 4
โข
((โตโ๐ด) =
โ
โ (โตโ๐ด) โบ (cfโ(cardโ(๐ต โm
(โตโ๐ด))))) |
117 | 116 | a1d 25 |
. . 3
โข
((โตโ๐ด) =
โ
โ (2o โผ ๐ต โ (โตโ๐ด) โบ (cfโ(cardโ(๐ต โm
(โตโ๐ด)))))) |
118 | 92, 117 | syl 17 |
. 2
โข (ยฌ
๐ด โ On โ
(2o โผ ๐ต
โ (โตโ๐ด)
โบ (cfโ(cardโ(๐ต โm (โตโ๐ด)))))) |
119 | 87, 118 | pm2.61i 182 |
1
โข
(2o โผ ๐ต โ (โตโ๐ด) โบ (cfโ(cardโ(๐ต โm
(โตโ๐ด))))) |