Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β π΄ β¦ (π΅ +o π₯)) = (π₯ β π΄ β¦ (π΅ +o π₯)) |
2 | 1 | oacomf1olem 8512 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β π΄ β¦ (π΅ +o π₯)):π΄β1-1-ontoβran
(π₯ β π΄ β¦ (π΅ +o π₯)) β§ (ran (π₯ β π΄ β¦ (π΅ +o π₯)) β© π΅) = β
)) |
3 | 2 | simpld 496 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (π₯ β π΄ β¦ (π΅ +o π₯)):π΄β1-1-ontoβran
(π₯ β π΄ β¦ (π΅ +o π₯))) |
4 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π΅ β¦ (π΄ +o π₯)) = (π₯ β π΅ β¦ (π΄ +o π₯)) |
5 | 4 | oacomf1olem 8512 |
. . . . . . . 8
β’ ((π΅ β On β§ π΄ β On) β ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β§ (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
)) |
6 | 5 | ancoms 460 |
. . . . . . 7
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β§ (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
)) |
7 | 6 | simpld 496 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β (π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯))) |
8 | | f1ocnv 6797 |
. . . . . 6
β’ ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β β‘(π₯ β π΅ β¦ (π΄ +o π₯)):ran (π₯ β π΅ β¦ (π΄ +o π₯))β1-1-ontoβπ΅) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β β‘(π₯ β π΅ β¦ (π΄ +o π₯)):ran (π₯ β π΅ β¦ (π΄ +o π₯))β1-1-ontoβπ΅) |
10 | | incom 4162 |
. . . . . 6
β’ (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) |
11 | 6 | simprd 497 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
) |
12 | 10, 11 | eqtrid 2785 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = β
) |
13 | 2 | simprd 497 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (ran (π₯ β π΄ β¦ (π΅ +o π₯)) β© π΅) = β
) |
14 | | f1oun 6804 |
. . . . 5
β’ ((((π₯ β π΄ β¦ (π΅ +o π₯)):π΄β1-1-ontoβran
(π₯ β π΄ β¦ (π΅ +o π₯)) β§ β‘(π₯ β π΅ β¦ (π΄ +o π₯)):ran (π₯ β π΅ β¦ (π΄ +o π₯))β1-1-ontoβπ΅) β§ ((π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = β
β§ (ran (π₯ β π΄ β¦ (π΅ +o π₯)) β© π΅) = β
)) β ((π₯ β π΄ β¦ (π΅ +o π₯)) βͺ β‘(π₯ β π΅ β¦ (π΄ +o π₯))):(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅)) |
15 | 3, 9, 12, 13, 14 | syl22anc 838 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β π΄ β¦ (π΅ +o π₯)) βͺ β‘(π₯ β π΅ β¦ (π΄ +o π₯))):(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅)) |
16 | | oacomf1o.1 |
. . . . 5
β’ πΉ = ((π₯ β π΄ β¦ (π΅ +o π₯)) βͺ β‘(π₯ β π΅ β¦ (π΄ +o π₯))) |
17 | | f1oeq1 6773 |
. . . . 5
β’ (πΉ = ((π₯ β π΄ β¦ (π΅ +o π₯)) βͺ β‘(π₯ β π΅ β¦ (π΄ +o π₯))) β (πΉ:(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅) β ((π₯ β π΄ β¦ (π΅ +o π₯)) βͺ β‘(π₯ β π΅ β¦ (π΄ +o π₯))):(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅))) |
18 | 16, 17 | ax-mp 5 |
. . . 4
β’ (πΉ:(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅) β ((π₯ β π΄ β¦ (π΅ +o π₯)) βͺ β‘(π₯ β π΅ β¦ (π΄ +o π₯))):(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅)) |
19 | 15, 18 | sylibr 233 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β πΉ:(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅)) |
20 | | oarec 8510 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β (π΄ +o π΅) = (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
21 | 20 | f1oeq2d 6781 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (πΉ:(π΄ +o π΅)β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅) β πΉ:(π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅))) |
22 | 19, 21 | mpbird 257 |
. 2
β’ ((π΄ β On β§ π΅ β On) β πΉ:(π΄ +o π΅)β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅)) |
23 | | oarec 8510 |
. . . . 5
β’ ((π΅ β On β§ π΄ β On) β (π΅ +o π΄) = (π΅ βͺ ran (π₯ β π΄ β¦ (π΅ +o π₯)))) |
24 | 23 | ancoms 460 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β (π΅ +o π΄) = (π΅ βͺ ran (π₯ β π΄ β¦ (π΅ +o π₯)))) |
25 | | uncom 4114 |
. . . 4
β’ (π΅ βͺ ran (π₯ β π΄ β¦ (π΅ +o π₯))) = (ran (π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅) |
26 | 24, 25 | eqtrdi 2789 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (π΅ +o π΄) = (ran (π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅)) |
27 | 26 | f1oeq3d 6782 |
. 2
β’ ((π΄ β On β§ π΅ β On) β (πΉ:(π΄ +o π΅)β1-1-ontoβ(π΅ +o π΄) β πΉ:(π΄ +o π΅)β1-1-ontoβ(ran
(π₯ β π΄ β¦ (π΅ +o π₯)) βͺ π΅))) |
28 | 22, 27 | mpbird 257 |
1
β’ ((π΄ β On β§ π΅ β On) β πΉ:(π΄ +o π΅)β1-1-ontoβ(π΅ +o π΄)) |