Step | Hyp | Ref
| Expression |
1 | | f1f 6739 |
. . . 4
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄βΆπ΅) |
2 | 1 | frnd 6677 |
. . 3
β’ (πΉ:π΄β1-1βπ΅ β ran πΉ β π΅) |
3 | | f1f 6739 |
. . . 4
β’ (πΊ:πΆβ1-1βπ· β πΊ:πΆβΆπ·) |
4 | 3 | frnd 6677 |
. . 3
β’ (πΊ:πΆβ1-1βπ· β ran πΊ β π·) |
5 | | unss12 4143 |
. . 3
β’ ((ran
πΉ β π΅ β§ ran πΊ β π·) β (ran πΉ βͺ ran πΊ) β (π΅ βͺ π·)) |
6 | 2, 4, 5 | syl2an 597 |
. 2
β’ ((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β (ran πΉ βͺ ran πΊ) β (π΅ βͺ π·)) |
7 | | f1f1orn 6796 |
. . . . 5
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran
πΉ) |
8 | | f1f1orn 6796 |
. . . . 5
β’ (πΊ:πΆβ1-1βπ· β πΊ:πΆβ1-1-ontoβran
πΊ) |
9 | 7, 8 | anim12i 614 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β (πΉ:π΄β1-1-ontoβran
πΉ β§ πΊ:πΆβ1-1-ontoβran
πΊ)) |
10 | | simprl 770 |
. . . . 5
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ ((π΄ β© πΆ) = β
β§ (π΅ β© π·) = β
)) β (π΄ β© πΆ) = β
) |
11 | | ss2in 4197 |
. . . . . . . 8
β’ ((ran
πΉ β π΅ β§ ran πΊ β π·) β (ran πΉ β© ran πΊ) β (π΅ β© π·)) |
12 | 2, 4, 11 | syl2an 597 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β (ran πΉ β© ran πΊ) β (π΅ β© π·)) |
13 | | sseq0 4360 |
. . . . . . 7
β’ (((ran
πΉ β© ran πΊ) β (π΅ β© π·) β§ (π΅ β© π·) = β
) β (ran πΉ β© ran πΊ) = β
) |
14 | 12, 13 | sylan 581 |
. . . . . 6
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ (π΅ β© π·) = β
) β (ran πΉ β© ran πΊ) = β
) |
15 | 14 | adantrl 715 |
. . . . 5
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ ((π΄ β© πΆ) = β
β§ (π΅ β© π·) = β
)) β (ran πΉ β© ran πΊ) = β
) |
16 | 10, 15 | jca 513 |
. . . 4
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ ((π΄ β© πΆ) = β
β§ (π΅ β© π·) = β
)) β ((π΄ β© πΆ) = β
β§ (ran πΉ β© ran πΊ) = β
)) |
17 | | f1oun 6804 |
. . . 4
β’ (((πΉ:π΄β1-1-ontoβran
πΉ β§ πΊ:πΆβ1-1-ontoβran
πΊ) β§ ((π΄ β© πΆ) = β
β§ (ran πΉ β© ran πΊ) = β
)) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1-ontoβ(ran
πΉ βͺ ran πΊ)) |
18 | 9, 16, 17 | syl2an2r 684 |
. . 3
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ ((π΄ β© πΆ) = β
β§ (π΅ β© π·) = β
)) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1-ontoβ(ran
πΉ βͺ ran πΊ)) |
19 | | f1of1 6784 |
. . 3
β’ ((πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1-ontoβ(ran
πΉ βͺ ran πΊ) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(ran πΉ βͺ ran πΊ)) |
20 | 18, 19 | syl 17 |
. 2
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ ((π΄ β© πΆ) = β
β§ (π΅ β© π·) = β
)) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(ran πΉ βͺ ran πΊ)) |
21 | | f1ss 6745 |
. . 3
β’ (((πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(ran πΉ βͺ ran πΊ) β§ (ran πΉ βͺ ran πΊ) β (π΅ βͺ π·)) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(π΅ βͺ π·)) |
22 | 21 | ancoms 460 |
. 2
β’ (((ran
πΉ βͺ ran πΊ) β (π΅ βͺ π·) β§ (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(ran πΉ βͺ ran πΊ)) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(π΅ βͺ π·)) |
23 | 6, 20, 22 | syl2an2r 684 |
1
β’ (((πΉ:π΄β1-1βπ΅ β§ πΊ:πΆβ1-1βπ·) β§ ((π΄ β© πΆ) = β
β§ (π΅ β© π·) = β
)) β (πΉ βͺ πΊ):(π΄ βͺ πΆ)β1-1β(π΅ βͺ π·)) |