Step | Hyp | Ref
| Expression |
1 | | oaf1o 8514 |
. . . . . . 7
β’ (π΅ β On β (π₯ β On β¦ (π΅ +o π₯)):Onβ1-1-ontoβ(On
β π΅)) |
2 | 1 | adantl 483 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β (π₯ β On β¦ (π΅ +o π₯)):Onβ1-1-ontoβ(On
β π΅)) |
3 | | f1of1 6787 |
. . . . . 6
β’ ((π₯ β On β¦ (π΅ +o π₯)):Onβ1-1-ontoβ(On
β π΅) β (π₯ β On β¦ (π΅ +o π₯)):Onβ1-1β(On β π΅)) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (π₯ β On β¦ (π΅ +o π₯)):Onβ1-1β(On β π΅)) |
5 | | onss 7723 |
. . . . . 6
β’ (π΄ β On β π΄ β On) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β π΄ β On) |
7 | | f1ssres 6750 |
. . . . 5
β’ (((π₯ β On β¦ (π΅ +o π₯)):Onβ1-1β(On β π΅) β§ π΄ β On) β ((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄):π΄β1-1β(On β π΅)) |
8 | 4, 6, 7 | syl2anc 585 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄):π΄β1-1β(On β π΅)) |
9 | 6 | resmptd 5998 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄) = (π₯ β π΄ β¦ (π΅ +o π₯))) |
10 | | oacomf1olem.1 |
. . . . . 6
β’ πΉ = (π₯ β π΄ β¦ (π΅ +o π₯)) |
11 | 9, 10 | eqtr4di 2791 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄) = πΉ) |
12 | | f1eq1 6737 |
. . . . 5
β’ (((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄) = πΉ β (((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄):π΄β1-1β(On β π΅) β πΉ:π΄β1-1β(On β π΅))) |
13 | 11, 12 | syl 17 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β (((π₯ β On β¦ (π΅ +o π₯)) βΎ π΄):π΄β1-1β(On β π΅) β πΉ:π΄β1-1β(On β π΅))) |
14 | 8, 13 | mpbid 231 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β πΉ:π΄β1-1β(On β π΅)) |
15 | | f1f1orn 6799 |
. . 3
β’ (πΉ:π΄β1-1β(On β π΅) β πΉ:π΄β1-1-ontoβran
πΉ) |
16 | 14, 15 | syl 17 |
. 2
β’ ((π΄ β On β§ π΅ β On) β πΉ:π΄β1-1-ontoβran
πΉ) |
17 | | f1f 6742 |
. . . 4
β’ (πΉ:π΄β1-1β(On β π΅) β πΉ:π΄βΆ(On β π΅)) |
18 | | frn 6679 |
. . . 4
β’ (πΉ:π΄βΆ(On β π΅) β ran πΉ β (On β π΅)) |
19 | 14, 17, 18 | 3syl 18 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β ran πΉ β (On β π΅)) |
20 | 19 | difss2d 4098 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β ran πΉ β On) |
21 | | reldisj 4415 |
. . . 4
β’ (ran
πΉ β On β ((ran
πΉ β© π΅) = β
β ran πΉ β (On β π΅))) |
22 | 20, 21 | syl 17 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β ((ran πΉ β© π΅) = β
β ran πΉ β (On β π΅))) |
23 | 19, 22 | mpbird 257 |
. 2
β’ ((π΄ β On β§ π΅ β On) β (ran πΉ β© π΅) = β
) |
24 | 16, 23 | jca 513 |
1
β’ ((π΄ β On β§ π΅ β On) β (πΉ:π΄β1-1-ontoβran
πΉ β§ (ran πΉ β© π΅) = β
)) |