Step | Hyp | Ref
| Expression |
1 | | marypha2.a |
. . 3
β’ (π β π΄ β Fin) |
2 | | marypha2.b |
. . . 4
β’ (π β πΉ:π΄βΆFin) |
3 | 2, 1 | unirnffid 9295 |
. . 3
β’ (π β βͺ ran πΉ β Fin) |
4 | | eqid 2737 |
. . . . 5
β’ βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) = βͺ
π₯ β π΄ ({π₯} Γ (πΉβπ₯)) |
5 | 4 | marypha2lem1 9378 |
. . . 4
β’ βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β (π΄ Γ βͺ ran
πΉ) |
6 | 5 | a1i 11 |
. . 3
β’ (π β βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β (π΄ Γ βͺ ran
πΉ)) |
7 | | marypha2.c |
. . . 4
β’ ((π β§ π β π΄) β π βΌ βͺ (πΉ β π)) |
8 | 2 | ffnd 6674 |
. . . . 5
β’ (π β πΉ Fn π΄) |
9 | 4 | marypha2lem4 9381 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π β π΄) β (βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β π) = βͺ (πΉ β π)) |
10 | 8, 9 | sylan 581 |
. . . 4
β’ ((π β§ π β π΄) β (βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β π) = βͺ (πΉ β π)) |
11 | 7, 10 | breqtrrd 5138 |
. . 3
β’ ((π β§ π β π΄) β π βΌ (βͺ
π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β π)) |
12 | 1, 3, 6, 11 | marypha1 9377 |
. 2
β’ (π β βπ β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯))π:π΄β1-1ββͺ ran πΉ) |
13 | | df-rex 3075 |
. . 3
β’
(βπ β
π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯))π:π΄β1-1ββͺ ran πΉ β βπ(π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) |
14 | | ssv 3973 |
. . . . . . . 8
β’ βͺ ran πΉ β V |
15 | | f1ss 6749 |
. . . . . . . 8
β’ ((π:π΄β1-1ββͺ ran πΉ β§ βͺ ran πΉ β V) β π:π΄β1-1βV) |
16 | 14, 15 | mpan2 690 |
. . . . . . 7
β’ (π:π΄β1-1ββͺ ran πΉ β π:π΄β1-1βV) |
17 | 16 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) β π:π΄β1-1βV) |
18 | | elpwi 4572 |
. . . . . . . 8
β’ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β π β βͺ
π₯ β π΄ ({π₯} Γ (πΉβπ₯))) |
19 | 18 | ad2antrl 727 |
. . . . . . 7
β’ ((π β§ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) β π β βͺ
π₯ β π΄ ({π₯} Γ (πΉβπ₯))) |
20 | | f1fn 6744 |
. . . . . . . . 9
β’ (π:π΄β1-1ββͺ ran πΉ β π Fn π΄) |
21 | 20 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) β π Fn π΄) |
22 | 4 | marypha2lem3 9380 |
. . . . . . . 8
β’ ((πΉ Fn π΄ β§ π Fn π΄) β (π β βͺ
π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β βπ₯ β π΄ (πβπ₯) β (πΉβπ₯))) |
23 | 8, 21, 22 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) β (π β βͺ
π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β βπ₯ β π΄ (πβπ₯) β (πΉβπ₯))) |
24 | 19, 23 | mpbid 231 |
. . . . . 6
β’ ((π β§ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) β βπ₯ β π΄ (πβπ₯) β (πΉβπ₯)) |
25 | 17, 24 | jca 513 |
. . . . 5
β’ ((π β§ (π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ)) β (π:π΄β1-1βV β§ βπ₯ β π΄ (πβπ₯) β (πΉβπ₯))) |
26 | 25 | ex 414 |
. . . 4
β’ (π β ((π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ) β (π:π΄β1-1βV β§ βπ₯ β π΄ (πβπ₯) β (πΉβπ₯)))) |
27 | 26 | eximdv 1921 |
. . 3
β’ (π β (βπ(π β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β§ π:π΄β1-1ββͺ ran πΉ) β βπ(π:π΄β1-1βV β§ βπ₯ β π΄ (πβπ₯) β (πΉβπ₯)))) |
28 | 13, 27 | biimtrid 241 |
. 2
β’ (π β (βπ β π« βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯))π:π΄β1-1ββͺ ran πΉ β βπ(π:π΄β1-1βV β§ βπ₯ β π΄ (πβπ₯) β (πΉβπ₯)))) |
29 | 12, 28 | mpd 15 |
1
β’ (π β βπ(π:π΄β1-1βV β§ βπ₯ β π΄ (πβπ₯) β (πΉβπ₯))) |