Step | Hyp | Ref
| Expression |
1 | | enrefg 8930 |
. . . . 5
β’ (π΄ β On β π΄ β π΄) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β π΄ β π΄) |
3 | | simpr 486 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β π΅ β On) |
4 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β π΅ β¦ (π΄ +o π₯)) = (π₯ β π΅ β¦ (π΄ +o π₯)) |
5 | 4 | oacomf1olem 8515 |
. . . . . . 7
β’ ((π΅ β On β§ π΄ β On) β ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β§ (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
)) |
6 | 5 | ancoms 460 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β§ (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
)) |
7 | 6 | simpld 496 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯))) |
8 | | f1oeng 8917 |
. . . . 5
β’ ((π΅ β On β§ (π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯))) β π΅ β ran (π₯ β π΅ β¦ (π΄ +o π₯))) |
9 | 3, 7, 8 | syl2anc 585 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β π΅ β ran (π₯ β π΅ β¦ (π΄ +o π₯))) |
10 | | incom 4165 |
. . . . 5
β’ (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) |
11 | 6 | simprd 497 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
) |
12 | 10, 11 | eqtrid 2785 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = β
) |
13 | | djuenun 10114 |
. . . 4
β’ ((π΄ β π΄ β§ π΅ β ran (π₯ β π΅ β¦ (π΄ +o π₯)) β§ (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = β
) β (π΄ β π΅) β (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
14 | 2, 9, 12, 13 | syl3anc 1372 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅) β (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
15 | | oarec 8513 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (π΄ +o π΅) = (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
16 | 14, 15 | breqtrrd 5137 |
. 2
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅) β (π΄ +o π΅)) |
17 | 16 | ensymd 8951 |
1
β’ ((π΄ β On β§ π΅ β On) β (π΄ +o π΅) β (π΄ β π΅)) |