Step | Hyp | Ref
| Expression |
1 | | dmresv 6153 |
. 2
β’ dom
(π΄ βΎ V) = dom π΄ |
2 | | resss 5963 |
. . . . 5
β’ (π΄ βΎ V) β π΄ |
3 | | ctex 8904 |
. . . . 5
β’ (π΄ βΌ Ο β π΄ β V) |
4 | | ssexg 5281 |
. . . . 5
β’ (((π΄ βΎ V) β π΄ β§ π΄ β V) β (π΄ βΎ V) β V) |
5 | 2, 3, 4 | sylancr 588 |
. . . 4
β’ (π΄ βΌ Ο β (π΄ βΎ V) β
V) |
6 | | fvex 6856 |
. . . . . . 7
β’
(1st βπ₯) β V |
7 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)) = (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)) |
8 | 6, 7 | fnmpti 6645 |
. . . . . 6
β’ (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)) Fn (π΄ βΎ V) |
9 | | dffn4 6763 |
. . . . . 6
β’ ((π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)) Fn (π΄ βΎ V) β (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβran (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯))) |
10 | 8, 9 | mpbi 229 |
. . . . 5
β’ (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβran (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)) |
11 | | relres 5967 |
. . . . . 6
β’ Rel
(π΄ βΎ
V) |
12 | | reldm 7977 |
. . . . . 6
β’ (Rel
(π΄ βΎ V) β dom
(π΄ βΎ V) = ran (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯))) |
13 | | foeq3 6755 |
. . . . . 6
β’ (dom
(π΄ βΎ V) = ran (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)) β ((π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβdom (π΄ βΎ V) β (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβran (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)))) |
14 | 11, 12, 13 | mp2b 10 |
. . . . 5
β’ ((π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβdom (π΄ βΎ V) β (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβran (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯))) |
15 | 10, 14 | mpbir 230 |
. . . 4
β’ (π₯ β (π΄ βΎ V) β¦ (1st
βπ₯)):(π΄ βΎ V)βontoβdom (π΄ βΎ V) |
16 | | fodomg 10459 |
. . . 4
β’ ((π΄ βΎ V) β V β
((π₯ β (π΄ βΎ V) β¦
(1st βπ₯)):(π΄ βΎ V)βontoβdom (π΄ βΎ V) β dom (π΄ βΎ V) βΌ (π΄ βΎ V))) |
17 | 5, 15, 16 | mpisyl 21 |
. . 3
β’ (π΄ βΌ Ο β dom
(π΄ βΎ V) βΌ
(π΄ βΎ
V)) |
18 | | ssdomg 8941 |
. . . . 5
β’ (π΄ β V β ((π΄ βΎ V) β π΄ β (π΄ βΎ V) βΌ π΄)) |
19 | 3, 2, 18 | mpisyl 21 |
. . . 4
β’ (π΄ βΌ Ο β (π΄ βΎ V) βΌ π΄) |
20 | | domtr 8948 |
. . . 4
β’ (((π΄ βΎ V) βΌ π΄ β§ π΄ βΌ Ο) β (π΄ βΎ V) βΌ
Ο) |
21 | 19, 20 | mpancom 687 |
. . 3
β’ (π΄ βΌ Ο β (π΄ βΎ V) βΌ
Ο) |
22 | | domtr 8948 |
. . 3
β’ ((dom
(π΄ βΎ V) βΌ
(π΄ βΎ V) β§ (π΄ βΎ V) βΌ Ο)
β dom (π΄ βΎ V)
βΌ Ο) |
23 | 17, 21, 22 | syl2anc 585 |
. 2
β’ (π΄ βΌ Ο β dom
(π΄ βΎ V) βΌ
Ο) |
24 | 1, 23 | eqbrtrrid 5142 |
1
β’ (π΄ βΌ Ο β dom
π΄ βΌ
Ο) |