Step | Hyp | Ref
| Expression |
1 | | ordom 7816 |
. . . . . 6
β’ Ord
Ο |
2 | | reldom 8895 |
. . . . . . . 8
β’ Rel
βΌ |
3 | 2 | brrelex2i 5693 |
. . . . . . 7
β’ (π΅ βΌ Ο β Ο
β V) |
4 | | elong 6329 |
. . . . . . 7
β’ (Ο
β V β (Ο β On β Ord Ο)) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π΅ βΌ Ο β (Ο
β On β Ord Ο)) |
6 | 1, 5 | mpbiri 258 |
. . . . 5
β’ (π΅ βΌ Ο β Ο
β On) |
7 | | ondomen 9981 |
. . . . 5
β’ ((Ο
β On β§ π΅ βΌ
Ο) β π΅ β
dom card) |
8 | 6, 7 | mpancom 687 |
. . . 4
β’ (π΅ βΌ Ο β π΅ β dom
card) |
9 | | eqid 2733 |
. . . . 5
β’ (π₯ β π΅ β¦ πΆ) = (π₯ β π΅ β¦ πΆ) |
10 | 9 | dmmptss 6197 |
. . . 4
β’ dom
(π₯ β π΅ β¦ πΆ) β π΅ |
11 | | ssnum 9983 |
. . . 4
β’ ((π΅ β dom card β§ dom
(π₯ β π΅ β¦ πΆ) β π΅) β dom (π₯ β π΅ β¦ πΆ) β dom card) |
12 | 8, 10, 11 | sylancl 587 |
. . 3
β’ (π΅ βΌ Ο β dom
(π₯ β π΅ β¦ πΆ) β dom card) |
13 | | funmpt 6543 |
. . . 4
β’ Fun
(π₯ β π΅ β¦ πΆ) |
14 | | funforn 6767 |
. . . 4
β’ (Fun
(π₯ β π΅ β¦ πΆ) β (π₯ β π΅ β¦ πΆ):dom (π₯ β π΅ β¦ πΆ)βontoβran (π₯ β π΅ β¦ πΆ)) |
15 | 13, 14 | mpbi 229 |
. . 3
β’ (π₯ β π΅ β¦ πΆ):dom (π₯ β π΅ β¦ πΆ)βontoβran (π₯ β π΅ β¦ πΆ) |
16 | | fodomnum 10001 |
. . 3
β’ (dom
(π₯ β π΅ β¦ πΆ) β dom card β ((π₯ β π΅ β¦ πΆ):dom (π₯ β π΅ β¦ πΆ)βontoβran (π₯ β π΅ β¦ πΆ) β ran (π₯ β π΅ β¦ πΆ) βΌ dom (π₯ β π΅ β¦ πΆ))) |
17 | 12, 15, 16 | mpisyl 21 |
. 2
β’ (π΅ βΌ Ο β ran
(π₯ β π΅ β¦ πΆ) βΌ dom (π₯ β π΅ β¦ πΆ)) |
18 | | ctex 8909 |
. . . 4
β’ (π΅ βΌ Ο β π΅ β V) |
19 | | ssdomg 8946 |
. . . 4
β’ (π΅ β V β (dom (π₯ β π΅ β¦ πΆ) β π΅ β dom (π₯ β π΅ β¦ πΆ) βΌ π΅)) |
20 | 18, 10, 19 | mpisyl 21 |
. . 3
β’ (π΅ βΌ Ο β dom
(π₯ β π΅ β¦ πΆ) βΌ π΅) |
21 | | domtr 8953 |
. . 3
β’ ((dom
(π₯ β π΅ β¦ πΆ) βΌ π΅ β§ π΅ βΌ Ο) β dom (π₯ β π΅ β¦ πΆ) βΌ Ο) |
22 | 20, 21 | mpancom 687 |
. 2
β’ (π΅ βΌ Ο β dom
(π₯ β π΅ β¦ πΆ) βΌ Ο) |
23 | | domtr 8953 |
. 2
β’ ((ran
(π₯ β π΅ β¦ πΆ) βΌ dom (π₯ β π΅ β¦ πΆ) β§ dom (π₯ β π΅ β¦ πΆ) βΌ Ο) β ran (π₯ β π΅ β¦ πΆ) βΌ Ο) |
24 | 17, 22, 23 | syl2anc 585 |
1
β’ (π΅ βΌ Ο β ran
(π₯ β π΅ β¦ πΆ) βΌ Ο) |