Step | Hyp | Ref
| Expression |
1 | | enrefg 8979 |
. . . . 5
β’ (π΄ β On β π΄ β π΄) |
2 | 1 | adantr 481 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β π΄ β π΄) |
3 | | simpr 485 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β π΅ β On) |
4 | | eqid 2732 |
. . . . . . . 8
β’ (π₯ β π΅ β¦ (π΄ +o π₯)) = (π₯ β π΅ β¦ (π΄ +o π₯)) |
5 | 4 | oacomf1olem 8563 |
. . . . . . 7
β’ ((π΅ β On β§ π΄ β On) β ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β§ (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
)) |
6 | 5 | ancoms 459 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On) β ((π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯)) β§ (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
)) |
7 | 6 | simpld 495 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯))) |
8 | | f1oeng 8966 |
. . . . 5
β’ ((π΅ β On β§ (π₯ β π΅ β¦ (π΄ +o π₯)):π΅β1-1-ontoβran
(π₯ β π΅ β¦ (π΄ +o π₯))) β π΅ β ran (π₯ β π΅ β¦ (π΄ +o π₯))) |
9 | 3, 7, 8 | syl2anc 584 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β π΅ β ran (π₯ β π΅ β¦ (π΄ +o π₯))) |
10 | | incom 4201 |
. . . . 5
β’ (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) |
11 | 6 | simprd 496 |
. . . . 5
β’ ((π΄ β On β§ π΅ β On) β (ran (π₯ β π΅ β¦ (π΄ +o π₯)) β© π΄) = β
) |
12 | 10, 11 | eqtrid 2784 |
. . . 4
β’ ((π΄ β On β§ π΅ β On) β (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = β
) |
13 | | djuenun 10164 |
. . . 4
β’ ((π΄ β π΄ β§ π΅ β ran (π₯ β π΅ β¦ (π΄ +o π₯)) β§ (π΄ β© ran (π₯ β π΅ β¦ (π΄ +o π₯))) = β
) β (π΄ β π΅) β (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
14 | 2, 9, 12, 13 | syl3anc 1371 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅) β (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
15 | | oarec 8561 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (π΄ +o π΅) = (π΄ βͺ ran (π₯ β π΅ β¦ (π΄ +o π₯)))) |
16 | 14, 15 | breqtrrd 5176 |
. 2
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅) β (π΄ +o π΅)) |
17 | 16 | ensymd 9000 |
1
β’ ((π΄ β On β§ π΅ β On) β (π΄ +o π΅) β (π΄ β π΅)) |