Step |
Hyp |
Ref |
Expression |
1 |
|
brrestrict.1 |
|- A e. _V |
2 |
|
brrestrict.2 |
|- B e. _V |
3 |
|
brrestrict.3 |
|- C e. _V |
4 |
|
opex |
|- <. A , B >. e. _V |
5 |
4 3
|
brco |
|- ( <. A , B >. ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) C <-> E. x ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x /\ x Cap C ) ) |
6 |
4
|
brtxp2 |
|- ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x <-> E. a E. b ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b ) ) |
7 |
|
3anrot |
|- ( ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b ) <-> ( <. A , B >. 1st a /\ <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b /\ x = <. a , b >. ) ) |
8 |
1 2
|
br1steq |
|- ( <. A , B >. 1st a <-> a = A ) |
9 |
|
vex |
|- b e. _V |
10 |
4 9
|
brco |
|- ( <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b <-> E. x ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) ) |
11 |
4
|
brtxp2 |
|- ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x <-> E. a E. b ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b ) ) |
12 |
|
3anrot |
|- ( ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b ) <-> ( <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b /\ x = <. a , b >. ) ) |
13 |
1 2
|
br2ndeq |
|- ( <. A , B >. 2nd a <-> a = B ) |
14 |
4 9
|
brco |
|- ( <. A , B >. ( Range o. 1st ) b <-> E. x ( <. A , B >. 1st x /\ x Range b ) ) |
15 |
1 2
|
br1steq |
|- ( <. A , B >. 1st x <-> x = A ) |
16 |
15
|
anbi1i |
|- ( ( <. A , B >. 1st x /\ x Range b ) <-> ( x = A /\ x Range b ) ) |
17 |
16
|
exbii |
|- ( E. x ( <. A , B >. 1st x /\ x Range b ) <-> E. x ( x = A /\ x Range b ) ) |
18 |
|
breq1 |
|- ( x = A -> ( x Range b <-> A Range b ) ) |
19 |
1 18
|
ceqsexv |
|- ( E. x ( x = A /\ x Range b ) <-> A Range b ) |
20 |
17 19
|
bitri |
|- ( E. x ( <. A , B >. 1st x /\ x Range b ) <-> A Range b ) |
21 |
1 9
|
brrange |
|- ( A Range b <-> b = ran A ) |
22 |
14 20 21
|
3bitri |
|- ( <. A , B >. ( Range o. 1st ) b <-> b = ran A ) |
23 |
|
biid |
|- ( x = <. a , b >. <-> x = <. a , b >. ) |
24 |
13 22 23
|
3anbi123i |
|- ( ( <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b /\ x = <. a , b >. ) <-> ( a = B /\ b = ran A /\ x = <. a , b >. ) ) |
25 |
12 24
|
bitri |
|- ( ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b ) <-> ( a = B /\ b = ran A /\ x = <. a , b >. ) ) |
26 |
25
|
2exbii |
|- ( E. a E. b ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b ) <-> E. a E. b ( a = B /\ b = ran A /\ x = <. a , b >. ) ) |
27 |
1
|
rnex |
|- ran A e. _V |
28 |
|
opeq1 |
|- ( a = B -> <. a , b >. = <. B , b >. ) |
29 |
28
|
eqeq2d |
|- ( a = B -> ( x = <. a , b >. <-> x = <. B , b >. ) ) |
30 |
|
opeq2 |
|- ( b = ran A -> <. B , b >. = <. B , ran A >. ) |
31 |
30
|
eqeq2d |
|- ( b = ran A -> ( x = <. B , b >. <-> x = <. B , ran A >. ) ) |
32 |
2 27 29 31
|
ceqsex2v |
|- ( E. a E. b ( a = B /\ b = ran A /\ x = <. a , b >. ) <-> x = <. B , ran A >. ) |
33 |
11 26 32
|
3bitri |
|- ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x <-> x = <. B , ran A >. ) |
34 |
33
|
anbi1i |
|- ( ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) <-> ( x = <. B , ran A >. /\ x Cart b ) ) |
35 |
34
|
exbii |
|- ( E. x ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) <-> E. x ( x = <. B , ran A >. /\ x Cart b ) ) |
36 |
|
opex |
|- <. B , ran A >. e. _V |
37 |
|
breq1 |
|- ( x = <. B , ran A >. -> ( x Cart b <-> <. B , ran A >. Cart b ) ) |
38 |
36 37
|
ceqsexv |
|- ( E. x ( x = <. B , ran A >. /\ x Cart b ) <-> <. B , ran A >. Cart b ) |
39 |
35 38
|
bitri |
|- ( E. x ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) <-> <. B , ran A >. Cart b ) |
40 |
2 27 9
|
brcart |
|- ( <. B , ran A >. Cart b <-> b = ( B X. ran A ) ) |
41 |
10 39 40
|
3bitri |
|- ( <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b <-> b = ( B X. ran A ) ) |
42 |
8 41 23
|
3anbi123i |
|- ( ( <. A , B >. 1st a /\ <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b /\ x = <. a , b >. ) <-> ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) ) |
43 |
7 42
|
bitri |
|- ( ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b ) <-> ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) ) |
44 |
43
|
2exbii |
|- ( E. a E. b ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b ) <-> E. a E. b ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) ) |
45 |
2 27
|
xpex |
|- ( B X. ran A ) e. _V |
46 |
|
opeq1 |
|- ( a = A -> <. a , b >. = <. A , b >. ) |
47 |
46
|
eqeq2d |
|- ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) ) |
48 |
|
opeq2 |
|- ( b = ( B X. ran A ) -> <. A , b >. = <. A , ( B X. ran A ) >. ) |
49 |
48
|
eqeq2d |
|- ( b = ( B X. ran A ) -> ( x = <. A , b >. <-> x = <. A , ( B X. ran A ) >. ) ) |
50 |
1 45 47 49
|
ceqsex2v |
|- ( E. a E. b ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) <-> x = <. A , ( B X. ran A ) >. ) |
51 |
6 44 50
|
3bitri |
|- ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x <-> x = <. A , ( B X. ran A ) >. ) |
52 |
51
|
anbi1i |
|- ( ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x /\ x Cap C ) <-> ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) ) |
53 |
52
|
exbii |
|- ( E. x ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x /\ x Cap C ) <-> E. x ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) ) |
54 |
5 53
|
bitri |
|- ( <. A , B >. ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) C <-> E. x ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) ) |
55 |
|
opex |
|- <. A , ( B X. ran A ) >. e. _V |
56 |
|
breq1 |
|- ( x = <. A , ( B X. ran A ) >. -> ( x Cap C <-> <. A , ( B X. ran A ) >. Cap C ) ) |
57 |
55 56
|
ceqsexv |
|- ( E. x ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) <-> <. A , ( B X. ran A ) >. Cap C ) |
58 |
1 45 3
|
brcap |
|- ( <. A , ( B X. ran A ) >. Cap C <-> C = ( A i^i ( B X. ran A ) ) ) |
59 |
54 57 58
|
3bitri |
|- ( <. A , B >. ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) C <-> C = ( A i^i ( B X. ran A ) ) ) |
60 |
|
df-restrict |
|- Restrict = ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) |
61 |
60
|
breqi |
|- ( <. A , B >. Restrict C <-> <. A , B >. ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) C ) |
62 |
|
dfres3 |
|- ( A |` B ) = ( A i^i ( B X. ran A ) ) |
63 |
62
|
eqeq2i |
|- ( C = ( A |` B ) <-> C = ( A i^i ( B X. ran A ) ) ) |
64 |
59 61 63
|
3bitr4i |
|- ( <. A , B >. Restrict C <-> C = ( A |` B ) ) |