Step |
Hyp |
Ref |
Expression |
1 |
|
brtpos2 |
|- ( C e. V -> ( <. A , B >. tpos F C <-> ( <. A , B >. e. ( `' dom F u. { (/) } ) /\ U. `' { <. A , B >. } F C ) ) ) |
2 |
1
|
adantr |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. A , B >. tpos F C <-> ( <. A , B >. e. ( `' dom F u. { (/) } ) /\ U. `' { <. A , B >. } F C ) ) ) |
3 |
|
opex |
|- <. B , A >. e. _V |
4 |
|
breldmg |
|- ( ( <. B , A >. e. _V /\ C e. V /\ <. B , A >. F C ) -> <. B , A >. e. dom F ) |
5 |
4
|
3expia |
|- ( ( <. B , A >. e. _V /\ C e. V ) -> ( <. B , A >. F C -> <. B , A >. e. dom F ) ) |
6 |
3 5
|
mpan |
|- ( C e. V -> ( <. B , A >. F C -> <. B , A >. e. dom F ) ) |
7 |
6
|
adantr |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. B , A >. F C -> <. B , A >. e. dom F ) ) |
8 |
|
opelcnvg |
|- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. `' dom F <-> <. B , A >. e. dom F ) ) |
9 |
8
|
adantl |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. A , B >. e. `' dom F <-> <. B , A >. e. dom F ) ) |
10 |
7 9
|
sylibrd |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. B , A >. F C -> <. A , B >. e. `' dom F ) ) |
11 |
|
elun1 |
|- ( <. A , B >. e. `' dom F -> <. A , B >. e. ( `' dom F u. { (/) } ) ) |
12 |
10 11
|
syl6 |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. B , A >. F C -> <. A , B >. e. ( `' dom F u. { (/) } ) ) ) |
13 |
12
|
pm4.71rd |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. B , A >. F C <-> ( <. A , B >. e. ( `' dom F u. { (/) } ) /\ <. B , A >. F C ) ) ) |
14 |
|
opswap |
|- U. `' { <. A , B >. } = <. B , A >. |
15 |
14
|
breq1i |
|- ( U. `' { <. A , B >. } F C <-> <. B , A >. F C ) |
16 |
15
|
anbi2i |
|- ( ( <. A , B >. e. ( `' dom F u. { (/) } ) /\ U. `' { <. A , B >. } F C ) <-> ( <. A , B >. e. ( `' dom F u. { (/) } ) /\ <. B , A >. F C ) ) |
17 |
13 16
|
bitr4di |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. B , A >. F C <-> ( <. A , B >. e. ( `' dom F u. { (/) } ) /\ U. `' { <. A , B >. } F C ) ) ) |
18 |
2 17
|
bitr4d |
|- ( ( C e. V /\ ( A e. _V /\ B e. _V ) ) -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) ) |
19 |
18
|
ex |
|- ( C e. V -> ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) ) ) |
20 |
|
brtpos0 |
|- ( C e. V -> ( (/) tpos F C <-> (/) F C ) ) |
21 |
|
opprc |
|- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) ) |
22 |
21
|
breq1d |
|- ( -. ( A e. _V /\ B e. _V ) -> ( <. A , B >. tpos F C <-> (/) tpos F C ) ) |
23 |
|
ancom |
|- ( ( A e. _V /\ B e. _V ) <-> ( B e. _V /\ A e. _V ) ) |
24 |
|
opprc |
|- ( -. ( B e. _V /\ A e. _V ) -> <. B , A >. = (/) ) |
25 |
24
|
breq1d |
|- ( -. ( B e. _V /\ A e. _V ) -> ( <. B , A >. F C <-> (/) F C ) ) |
26 |
23 25
|
sylnbi |
|- ( -. ( A e. _V /\ B e. _V ) -> ( <. B , A >. F C <-> (/) F C ) ) |
27 |
22 26
|
bibi12d |
|- ( -. ( A e. _V /\ B e. _V ) -> ( ( <. A , B >. tpos F C <-> <. B , A >. F C ) <-> ( (/) tpos F C <-> (/) F C ) ) ) |
28 |
20 27
|
syl5ibrcom |
|- ( C e. V -> ( -. ( A e. _V /\ B e. _V ) -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) ) ) |
29 |
19 28
|
pm2.61d |
|- ( C e. V -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) ) |