Step | Hyp | Ref
| Expression |
1 | | opeq 4619 |
. . . . 5
Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) |
2 | 1 | breq1i 4646 |
. . . 4
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 ![x](_x.gif) ![)](rp.gif) |
3 | | brco 4883 |
. . . 4
![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) ![>.](rangle.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | vex 2862 |
. . . . . . . . . 10
![_V](rmcv.gif) |
5 | 4 | proj1ex 4593 |
. . . . . . . . 9
Proj1 ![_V](rmcv.gif) |
6 | 4 | proj2ex 4594 |
. . . . . . . . 9
Proj2 ![_V](rmcv.gif) |
7 | 5, 6 | opbr1st 5501 |
. . . . . . . 8
![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) Proj1 ![t](_t.gif) ![)](rp.gif) |
8 | | eqcom 2355 |
. . . . . . . 8
Proj1
Proj1 ![y](_y.gif) ![)](rp.gif) |
9 | 7, 8 | bitri 240 |
. . . . . . 7
![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) Proj1 ![y](_y.gif) ![)](rp.gif) |
10 | 9 | anbi1i 676 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 ![x](_x.gif) ![(](lp.gif)
Proj1 ![t](_t.gif) Proj1 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | exbii 1582 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
Proj1 ![t](_t.gif) Proj1 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | breq1 4642 |
. . . . . . 7
![(](lp.gif) Proj1 ![(](lp.gif) ![t](_t.gif)
Proj1 Proj1 ![y](_y.gif) Proj1 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | opeq 4619 |
. . . . . . . . 9
Proj1 Proj1 Proj1 ![y](_y.gif) Proj2 Proj1 ![y](_y.gif) ![>.](rangle.gif) |
14 | 13 | breq1i 4646 |
. . . . . . . 8
Proj1
![y](_y.gif)
Proj1 Proj1 Proj1 ![y](_y.gif) Proj2 Proj1 ![y](_y.gif) ![>.](rangle.gif)
Proj1 ![x](_x.gif) ![)](rp.gif) |
15 | 5 | proj1ex 4593 |
. . . . . . . . 9
Proj1 Proj1 ![_V](rmcv.gif) |
16 | 5 | proj2ex 4594 |
. . . . . . . . 9
Proj2 Proj1 ![_V](rmcv.gif) |
17 | 15, 16 | opbr1st 5501 |
. . . . . . . 8
![(](lp.gif) Proj1
Proj1 ![y](_y.gif)
Proj2 Proj1 ![y](_y.gif) ![>.](rangle.gif) Proj1 Proj1 Proj1 Proj1 ![x](_x.gif) ![)](rp.gif) |
18 | 14, 17 | bitri 240 |
. . . . . . 7
Proj1
![y](_y.gif)
Proj1 Proj1 Proj1 Proj1 ![x](_x.gif) ![)](rp.gif) |
19 | 12, 18 | syl6bb 252 |
. . . . . 6
![(](lp.gif) Proj1 ![(](lp.gif) ![t](_t.gif)
Proj1 Proj1 Proj1 Proj1 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 5, 19 | ceqsexv 2894 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
Proj1 ![t](_t.gif) Proj1 ![x](_x.gif) Proj1 Proj1 Proj1 ![x](_x.gif) ![)](rp.gif) |
21 | 11, 20 | bitri 240 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 ![x](_x.gif) Proj1 Proj1 Proj1 ![x](_x.gif) ![)](rp.gif) |
22 | 2, 3, 21 | 3bitri 262 |
. . 3
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 Proj1
Proj1
Proj1 ![x](_x.gif) ![)](rp.gif) |
23 | | opeq 4619 |
. . . . 5
Proj2 Proj1 Proj2 ![x](_x.gif) Proj2
Proj2 ![x](_x.gif) ![>.](rangle.gif) |
24 | 23 | breq2i 4647 |
. . . 4
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) Proj2 ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Proj1
Proj2 ![x](_x.gif)
Proj2 Proj2 ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
25 | | trtxp 5781 |
. . . 4
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) Proj1 Proj2 ![x](_x.gif) Proj2 Proj2 ![x](_x.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 Proj2
![y](_y.gif) Proj2 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 1 | breq1i 4646 |
. . . . . 6
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1
Proj2 Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
27 | | brco 4883 |
. . . . . 6
![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) ![>.](rangle.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1
Proj2 ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif)
Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 9 | anbi1i 676 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 Proj2 ![x](_x.gif) ![(](lp.gif) Proj1 ![t](_t.gif) Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 Proj2 ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1 ![t](_t.gif) Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | breq1 4642 |
. . . . . . . . 9
![(](lp.gif) Proj1 ![(](lp.gif) ![t](_t.gif)
Proj1 Proj2 Proj1 ![y](_y.gif) Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 13 | breq1i 4646 |
. . . . . . . . . 10
Proj1
![y](_y.gif)
Proj1 Proj2 Proj1 Proj1 ![y](_y.gif) Proj2 Proj1 ![y](_y.gif) ![>.](rangle.gif) Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
32 | 15, 16 | opbr2nd 5502 |
. . . . . . . . . 10
![(](lp.gif) Proj1
Proj1 ![y](_y.gif)
Proj2 Proj1 ![y](_y.gif) ![>.](rangle.gif) Proj1 Proj2 Proj2 Proj1
Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
33 | 31, 32 | bitri 240 |
. . . . . . . . 9
Proj1
![y](_y.gif)
Proj1 Proj2 Proj2 Proj1 Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
34 | 30, 33 | syl6bb 252 |
. . . . . . . 8
![(](lp.gif) Proj1 ![(](lp.gif) ![t](_t.gif)
Proj1 Proj2 Proj2 Proj1 Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 5, 34 | ceqsexv 2894 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
Proj1 ![t](_t.gif) Proj1 Proj2 ![x](_x.gif) Proj2 Proj1 Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
36 | 29, 35 | bitri 240 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) ![1st](_1st.gif) ![t](_t.gif) Proj1 Proj2 ![x](_x.gif) Proj2 Proj1 Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
37 | 26, 27, 36 | 3bitri 262 |
. . . . 5
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1
Proj2 Proj2 Proj1 Proj1 Proj2 ![x](_x.gif) ![)](rp.gif) |
38 | 1 | breq1i 4646 |
. . . . . 6
![(](lp.gif) ![y](_y.gif) Proj2 Proj2 Proj1 ![y](_y.gif) Proj2 ![y](_y.gif) ![>.](rangle.gif) Proj2 Proj2
![x](_x.gif) ![)](rp.gif) |
39 | 5, 6 | opbr2nd 5502 |
. . . . . 6
![(](lp.gif) Proj1
![y](_y.gif)
Proj2 ![y](_y.gif) ![>.](rangle.gif) Proj2
Proj2 Proj2 Proj2 Proj2 ![x](_x.gif) ![)](rp.gif) |
40 | 38, 39 | bitri 240 |
. . . . 5
![(](lp.gif) ![y](_y.gif) Proj2 Proj2 Proj2 Proj2 Proj2
![x](_x.gif) ![)](rp.gif) |
41 | 37, 40 | anbi12i 678 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 Proj2
![y](_y.gif) Proj2 Proj2 ![x](_x.gif) Proj2
Proj1
Proj1 Proj2 Proj2
Proj2 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 24, 25, 41 | 3bitri 262 |
. . 3
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) Proj2 Proj2
Proj1
Proj1 Proj2 Proj2
Proj2 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 22, 42 | anbi12i 678 |
. 2
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) Proj2 ![x](_x.gif) Proj1 Proj1
Proj1 Proj2 Proj1 Proj1 Proj2 Proj2
Proj2 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | opeq 4619 |
. . . 4
Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) ![>.](rangle.gif) |
45 | 44 | breq2i 4647 |
. . 3
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
46 | | trtxp 5781 |
. . 3
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) Proj1 ![x](_x.gif) Proj2 ![x](_x.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 45, 46 | bitri 240 |
. 2
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![1st](_1st.gif) Proj1 ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
48 | | 3anass 938 |
. 2
![(](lp.gif) Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 ![x](_x.gif) Proj1 Proj1
Proj1 Proj2 Proj1 Proj1 Proj2 Proj2
Proj2 Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 43, 47, 48 | 3bitr4i 268 |
1
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif)
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) Proj1
Proj1
Proj1 Proj2 Proj1
Proj1 Proj2 Proj2 Proj2
Proj2 ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |