Step |
Hyp |
Ref |
Expression |
1 |
|
funcnvsn |
|- Fun `' { <. A , B >. } |
2 |
|
funcnvsn |
|- Fun `' { <. C , D >. } |
3 |
1 2
|
pm3.2i |
|- ( Fun `' { <. A , B >. } /\ Fun `' { <. C , D >. } ) |
4 |
|
df-rn |
|- ran { <. A , B >. } = dom `' { <. A , B >. } |
5 |
|
rnsnopg |
|- ( A e. U -> ran { <. A , B >. } = { B } ) |
6 |
4 5
|
syl5eqr |
|- ( A e. U -> dom `' { <. A , B >. } = { B } ) |
7 |
|
df-rn |
|- ran { <. C , D >. } = dom `' { <. C , D >. } |
8 |
|
rnsnopg |
|- ( C e. V -> ran { <. C , D >. } = { D } ) |
9 |
7 8
|
syl5eqr |
|- ( C e. V -> dom `' { <. C , D >. } = { D } ) |
10 |
6 9
|
ineqan12d |
|- ( ( A e. U /\ C e. V ) -> ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = ( { B } i^i { D } ) ) |
11 |
10
|
3adant3 |
|- ( ( A e. U /\ C e. V /\ B =/= D ) -> ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = ( { B } i^i { D } ) ) |
12 |
|
disjsn2 |
|- ( B =/= D -> ( { B } i^i { D } ) = (/) ) |
13 |
12
|
3ad2ant3 |
|- ( ( A e. U /\ C e. V /\ B =/= D ) -> ( { B } i^i { D } ) = (/) ) |
14 |
11 13
|
eqtrd |
|- ( ( A e. U /\ C e. V /\ B =/= D ) -> ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = (/) ) |
15 |
|
funun |
|- ( ( ( Fun `' { <. A , B >. } /\ Fun `' { <. C , D >. } ) /\ ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = (/) ) -> Fun ( `' { <. A , B >. } u. `' { <. C , D >. } ) ) |
16 |
3 14 15
|
sylancr |
|- ( ( A e. U /\ C e. V /\ B =/= D ) -> Fun ( `' { <. A , B >. } u. `' { <. C , D >. } ) ) |
17 |
|
df-pr |
|- { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } ) |
18 |
17
|
cnveqi |
|- `' { <. A , B >. , <. C , D >. } = `' ( { <. A , B >. } u. { <. C , D >. } ) |
19 |
|
cnvun |
|- `' ( { <. A , B >. } u. { <. C , D >. } ) = ( `' { <. A , B >. } u. `' { <. C , D >. } ) |
20 |
18 19
|
eqtri |
|- `' { <. A , B >. , <. C , D >. } = ( `' { <. A , B >. } u. `' { <. C , D >. } ) |
21 |
20
|
funeqi |
|- ( Fun `' { <. A , B >. , <. C , D >. } <-> Fun ( `' { <. A , B >. } u. `' { <. C , D >. } ) ) |
22 |
16 21
|
sylibr |
|- ( ( A e. U /\ C e. V /\ B =/= D ) -> Fun `' { <. A , B >. , <. C , D >. } ) |