Step | Hyp | Ref
| Expression |
1 | | dmresv 6156 |
. 2
β’ dom
(πΉ βΎ V) = dom πΉ |
2 | | finresfin 9220 |
. . . 4
β’ (πΉ β Fin β (πΉ βΎ V) β
Fin) |
3 | | fvex 6859 |
. . . . . . 7
β’
(1st βπ₯) β V |
4 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)) = (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)) |
5 | 3, 4 | fnmpti 6648 |
. . . . . 6
β’ (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)) Fn (πΉ βΎ V) |
6 | | dffn4 6766 |
. . . . . 6
β’ ((π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)) Fn (πΉ βΎ V) β (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβran (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯))) |
7 | 5, 6 | mpbi 229 |
. . . . 5
β’ (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβran (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)) |
8 | | relres 5970 |
. . . . . 6
β’ Rel
(πΉ βΎ
V) |
9 | | reldm 7980 |
. . . . . 6
β’ (Rel
(πΉ βΎ V) β dom
(πΉ βΎ V) = ran (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯))) |
10 | | foeq3 6758 |
. . . . . 6
β’ (dom
(πΉ βΎ V) = ran (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)) β ((π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβdom (πΉ βΎ V) β (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβran (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)))) |
11 | 8, 9, 10 | mp2b 10 |
. . . . 5
β’ ((π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβdom (πΉ βΎ V) β (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβran (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯))) |
12 | 7, 11 | mpbir 230 |
. . . 4
β’ (π₯ β (πΉ βΎ V) β¦ (1st
βπ₯)):(πΉ βΎ V)βontoβdom (πΉ βΎ V) |
13 | | fodomfi 9275 |
. . . 4
β’ (((πΉ βΎ V) β Fin β§
(π₯ β (πΉ βΎ V) β¦
(1st βπ₯)):(πΉ βΎ V)βontoβdom (πΉ βΎ V)) β dom (πΉ βΎ V) βΌ (πΉ βΎ V)) |
14 | 2, 12, 13 | sylancl 587 |
. . 3
β’ (πΉ β Fin β dom (πΉ βΎ V) βΌ (πΉ βΎ V)) |
15 | | resss 5966 |
. . . 4
β’ (πΉ βΎ V) β πΉ |
16 | | ssdomg 8946 |
. . . 4
β’ (πΉ β Fin β ((πΉ βΎ V) β πΉ β (πΉ βΎ V) βΌ πΉ)) |
17 | 15, 16 | mpi 20 |
. . 3
β’ (πΉ β Fin β (πΉ βΎ V) βΌ πΉ) |
18 | | domtr 8953 |
. . 3
β’ ((dom
(πΉ βΎ V) βΌ
(πΉ βΎ V) β§ (πΉ βΎ V) βΌ πΉ) β dom (πΉ βΎ V) βΌ πΉ) |
19 | 14, 17, 18 | syl2anc 585 |
. 2
β’ (πΉ β Fin β dom (πΉ βΎ V) βΌ πΉ) |
20 | 1, 19 | eqbrtrrid 5145 |
1
β’ (πΉ β Fin β dom πΉ βΌ πΉ) |