Step | Hyp | Ref
| Expression |
1 | | dffun2 5119 |
. . . 4
![(](lp.gif) Swap ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) Swap Swap
![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | opeq 4619 |
. . . . . . . 8
Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) |
3 | 2 | breq2i 4647 |
. . . . . . 7
![(](lp.gif) Swap Swap
Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
4 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
5 | 4 | proj1ex 4593 |
. . . . . . . 8
Proj1 ![_V](rmcv.gif) |
6 | 4 | proj2ex 4594 |
. . . . . . . 8
Proj2 ![_V](rmcv.gif) |
7 | 5, 6 | brswap2 4860 |
. . . . . . 7
![(](lp.gif) Swap Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) Proj2 ![y](_y.gif) Proj1 ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
8 | 3, 7 | bitri 240 |
. . . . . 6
![(](lp.gif) Swap Proj2 ![y](_y.gif) Proj1 ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
9 | | opeq 4619 |
. . . . . . . 8
Proj1 ![z](_z.gif) Proj2 ![z](_z.gif) ![>.](rangle.gif) |
10 | 9 | breq2i 4647 |
. . . . . . 7
![(](lp.gif) Swap Swap
Proj1 ![z](_z.gif) Proj2 ![z](_z.gif) ![>.](rangle.gif) ![)](rp.gif) |
11 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
12 | 11 | proj1ex 4593 |
. . . . . . . 8
Proj1 ![_V](rmcv.gif) |
13 | 11 | proj2ex 4594 |
. . . . . . . 8
Proj2 ![_V](rmcv.gif) |
14 | 12, 13 | brswap2 4860 |
. . . . . . 7
![(](lp.gif) Swap Proj1 ![z](_z.gif) Proj2 ![z](_z.gif) Proj2 ![z](_z.gif) Proj1 ![z](_z.gif) ![>.](rangle.gif) ![)](rp.gif) |
15 | 10, 14 | bitri 240 |
. . . . . 6
![(](lp.gif) Swap Proj2 ![z](_z.gif) Proj1 ![z](_z.gif) ![>.](rangle.gif) ![)](rp.gif) |
16 | | eqtr2 2371 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Proj2 ![y](_y.gif) Proj1 ![y](_y.gif) Proj2 ![z](_z.gif) Proj1 ![z](_z.gif) ![>.](rangle.gif) Proj2 ![y](_y.gif) Proj1 ![y](_y.gif) Proj2
![z](_z.gif)
Proj1 ![z](_z.gif) ![>.](rangle.gif) ![)](rp.gif) |
17 | | ancom 437 |
. . . . . . . 8
![(](lp.gif) Proj2 Proj2 Proj1
Proj1 ![z](_z.gif) Proj1
Proj1
Proj2
Proj2 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | opth 4602 |
. . . . . . . 8
![(](lp.gif) Proj2
![y](_y.gif)
Proj1 ![y](_y.gif) Proj2 ![z](_z.gif) Proj1 ![z](_z.gif) Proj2 Proj2 Proj1 Proj1 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 2, 9 | eqeq12i 2366 |
. . . . . . . . 9
![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) Proj1
![z](_z.gif)
Proj2 ![z](_z.gif) ![>.](rangle.gif) ![)](rp.gif) |
20 | | opth 4602 |
. . . . . . . . 9
![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) Proj1 ![z](_z.gif) Proj2 ![z](_z.gif) Proj1 Proj1 Proj2 Proj2 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 19, 20 | bitri 240 |
. . . . . . . 8
![(](lp.gif) Proj1
Proj1
Proj2
Proj2 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 17, 18, 21 | 3bitr4i 268 |
. . . . . . 7
![(](lp.gif) Proj2
![y](_y.gif)
Proj1 ![y](_y.gif) Proj2 ![z](_z.gif) Proj1 ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) |
23 | 16, 22 | sylib 188 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Proj2 ![y](_y.gif) Proj1 ![y](_y.gif) Proj2 ![z](_z.gif) Proj1 ![z](_z.gif) ![>.](rangle.gif) ![z](_z.gif) ![)](rp.gif) |
24 | 8, 15, 23 | syl2anb 465 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Swap Swap ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) |
25 | 24 | gen2 1547 |
. . . 4
![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) Swap Swap ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) |
26 | 1, 25 | mpgbir 1550 |
. . 3
Swap |
27 | | eqv 3565 |
. . . 4
![(](lp.gif) Swap ![A.](forall.gif)
Swap ![)](rp.gif) |
28 | | opeq 4619 |
. . . . 5
Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) ![>.](rangle.gif) |
29 | | eqid 2353 |
. . . . . . 7
Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) Proj1
![x](_x.gif)
Proj2 ![x](_x.gif) ![>.](rangle.gif) |
30 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
31 | 30 | proj2ex 4594 |
. . . . . . . 8
Proj2 ![_V](rmcv.gif) |
32 | 30 | proj1ex 4593 |
. . . . . . . 8
Proj1 ![_V](rmcv.gif) |
33 | 31, 32 | brswap2 4860 |
. . . . . . 7
![(](lp.gif) Proj1
![x](_x.gif)
Proj2 ![x](_x.gif) Swap Proj2 ![x](_x.gif) Proj1 ![x](_x.gif) Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
34 | 29, 33 | mpbir 200 |
. . . . . 6
Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) Swap Proj2 ![x](_x.gif) Proj1 ![x](_x.gif) ![>.](rangle.gif) |
35 | | breldm 4911 |
. . . . . 6
![(](lp.gif) Proj1
![x](_x.gif)
Proj2 ![x](_x.gif) Swap Proj2 ![x](_x.gif) Proj1 ![x](_x.gif) Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) Swap ![)](rp.gif) |
36 | 34, 35 | ax-mp 5 |
. . . . 5
Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) Swap
|
37 | 28, 36 | eqeltri 2423 |
. . . 4
Swap |
38 | 27, 37 | mpgbir 1550 |
. . 3
Swap ![_V](rmcv.gif) |
39 | | df-fn 4790 |
. . 3
Swap
![(](lp.gif) Swap Swap
![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 26, 38, 39 | mpbir2an 886 |
. 2
Swap ![_V](rmcv.gif) |
41 | | cnvswap 5510 |
. . . 4
Swap Swap |
42 | 41 | fneq1i 5178 |
. . 3
![(](lp.gif) Swap Swap ![_V](rmcv.gif) ![)](rp.gif) |
43 | 40, 42 | mpbir 200 |
. 2
Swap ![_V](rmcv.gif) |
44 | | dff1o4 5294 |
. 2
Swap
![:](colon.gif) ![_V](rmcv.gif) ![-1-1-onto->](onetooneonto.gif) Swap
Swap ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 40, 43, 44 | mpbir2an 886 |
1
Swap ![:](colon.gif) ![_V](rmcv.gif) ![-1-1-onto->](onetooneonto.gif) ![_V](rmcv.gif) |