Step |
Hyp |
Ref |
Expression |
1 |
|
df-xrn |
|- ( R |X. S ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) |
2 |
1
|
breqi |
|- ( A ( R |X. S ) <. B , C >. <-> A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. ) |
3 |
2
|
a1i |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. S ) <. B , C >. <-> A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. ) ) |
4 |
|
brin |
|- ( A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. <-> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. /\ A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. ) ) |
5 |
4
|
a1i |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. <-> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. /\ A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. ) ) ) |
6 |
|
opex |
|- <. B , C >. e. _V |
7 |
|
brcog |
|- ( ( A e. V /\ <. B , C >. e. _V ) -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) ) ) |
8 |
6 7
|
mpan2 |
|- ( A e. V -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) ) ) |
9 |
8
|
3ad2ant1 |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) ) ) |
10 |
|
brcnvg |
|- ( ( x e. _V /\ <. B , C >. e. _V ) -> ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 1st |` ( _V X. _V ) ) x ) ) |
11 |
6 10
|
mpan2 |
|- ( x e. _V -> ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 1st |` ( _V X. _V ) ) x ) ) |
12 |
11
|
elv |
|- ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 1st |` ( _V X. _V ) ) x ) |
13 |
|
brres |
|- ( x e. _V -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) ) |
14 |
13
|
elv |
|- ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) |
15 |
|
opelvvg |
|- ( ( B e. W /\ C e. X ) -> <. B , C >. e. ( _V X. _V ) ) |
16 |
15
|
biantrurd |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. 1st x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) ) |
17 |
14 16
|
bitr4id |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> <. B , C >. 1st x ) ) |
18 |
|
br1steqg |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. 1st x <-> x = B ) ) |
19 |
17 18
|
bitrd |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> x = B ) ) |
20 |
19
|
3adant1 |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> x = B ) ) |
21 |
12 20
|
syl5bb |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> x = B ) ) |
22 |
21
|
anbi1cd |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) <-> ( x = B /\ A R x ) ) ) |
23 |
22
|
exbidv |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) <-> E. x ( x = B /\ A R x ) ) ) |
24 |
|
breq2 |
|- ( x = B -> ( A R x <-> A R B ) ) |
25 |
24
|
ceqsexgv |
|- ( B e. W -> ( E. x ( x = B /\ A R x ) <-> A R B ) ) |
26 |
25
|
3ad2ant2 |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x ( x = B /\ A R x ) <-> A R B ) ) |
27 |
9 23 26
|
3bitrd |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> A R B ) ) |
28 |
|
brcog |
|- ( ( A e. V /\ <. B , C >. e. _V ) -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) ) ) |
29 |
6 28
|
mpan2 |
|- ( A e. V -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) ) ) |
30 |
29
|
3ad2ant1 |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) ) ) |
31 |
|
brcnvg |
|- ( ( y e. _V /\ <. B , C >. e. _V ) -> ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 2nd |` ( _V X. _V ) ) y ) ) |
32 |
6 31
|
mpan2 |
|- ( y e. _V -> ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 2nd |` ( _V X. _V ) ) y ) ) |
33 |
32
|
elv |
|- ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 2nd |` ( _V X. _V ) ) y ) |
34 |
|
brres |
|- ( y e. _V -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) ) |
35 |
34
|
elv |
|- ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) |
36 |
15
|
biantrurd |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. 2nd y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) ) |
37 |
35 36
|
bitr4id |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> <. B , C >. 2nd y ) ) |
38 |
|
br2ndeqg |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. 2nd y <-> y = C ) ) |
39 |
37 38
|
bitrd |
|- ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> y = C ) ) |
40 |
39
|
3adant1 |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> y = C ) ) |
41 |
33 40
|
syl5bb |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> y = C ) ) |
42 |
41
|
anbi1cd |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) <-> ( y = C /\ A S y ) ) ) |
43 |
42
|
exbidv |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) <-> E. y ( y = C /\ A S y ) ) ) |
44 |
|
breq2 |
|- ( y = C -> ( A S y <-> A S C ) ) |
45 |
44
|
ceqsexgv |
|- ( C e. X -> ( E. y ( y = C /\ A S y ) <-> A S C ) ) |
46 |
45
|
3ad2ant3 |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. y ( y = C /\ A S y ) <-> A S C ) ) |
47 |
30 43 46
|
3bitrd |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> A S C ) ) |
48 |
27 47
|
anbi12d |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. /\ A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. ) <-> ( A R B /\ A S C ) ) ) |
49 |
3 5 48
|
3bitrd |
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. S ) <. B , C >. <-> ( A R B /\ A S C ) ) ) |