Step | Hyp | Ref
| Expression |
1 | | df-op 4566 |
. . . . 5
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Phi ![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
2 | 1 | eleq2i 2417 |
. . . 4
![(](lp.gif) Phi 0c![}](rbrace.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) Phi
0c![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Phi
![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | elun 3220 |
. . . . 5
![(](lp.gif) Phi 0c![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Phi
![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
![{](lbrace.gif) ![E.](exists.gif)
Phi ![y](_y.gif) Phi 0c![}](rbrace.gif)
![{](lbrace.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
5 | 4 | phiex 4572 |
. . . . . . . 8
Phi ![_V](rmcv.gif) |
6 | | snex 4111 |
. . . . . . . 8
0c ![_V](rmcv.gif) |
7 | 5, 6 | unex 4106 |
. . . . . . 7
Phi
0c![}](rbrace.gif)
![_V](rmcv.gif) |
8 | | eqeq1 2359 |
. . . . . . . 8
![(](lp.gif) Phi 0c![}](rbrace.gif) ![(](lp.gif) Phi
Phi
0c![}](rbrace.gif)
Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | rexbidv 2635 |
. . . . . . 7
![(](lp.gif) Phi 0c![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif) Phi
![E.](exists.gif) Phi 0c![}](rbrace.gif) Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 7, 9 | elab 2985 |
. . . . . 6
![(](lp.gif) Phi 0c![}](rbrace.gif)
![{](lbrace.gif) ![E.](exists.gif)
Phi ![y](_y.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) Phi ![y](_y.gif) ![)](rp.gif) |
11 | | phi011 4599 |
. . . . . . . . 9
![(](lp.gif) Phi
0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | equcom 1680 |
. . . . . . . . 9
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) |
13 | 11, 12 | bitr3i 242 |
. . . . . . . 8
![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif)
![z](_z.gif) ![)](rp.gif) |
14 | 13 | rexbii 2639 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif)
![E.](exists.gif) ![z](_z.gif) ![)](rp.gif) |
15 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) Phi 0c![}](rbrace.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | rexbidv 2635 |
. . . . . . . 8
![(](lp.gif) Phi 0c![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif)
![E.](exists.gif) Phi 0c![}](rbrace.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 7, 16 | elab 2985 |
. . . . . . 7
![(](lp.gif) Phi 0c![}](rbrace.gif)
![{](lbrace.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | risset 2661 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![)](rp.gif) |
19 | 14, 17, 18 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) Phi 0c![}](rbrace.gif)
![{](lbrace.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![B](_cb.gif) ![)](rp.gif) |
20 | 10, 19 | orbi12i 507 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) ![{](lbrace.gif)
![E.](exists.gif) Phi
![y](_y.gif) Phi 0c![}](rbrace.gif) ![{](lbrace.gif)
![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 3, 20 | bitri 240 |
. . . 4
![(](lp.gif) Phi 0c![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Phi
![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 2, 21 | bitri 240 |
. . 3
![(](lp.gif) Phi 0c![}](rbrace.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | phieq 4570 |
. . . . . 6
![(](lp.gif)
Phi Phi
![z](_z.gif) ![)](rp.gif) |
24 | 23 | uneq1d 3417 |
. . . . 5
![(](lp.gif) Phi 0c![}](rbrace.gif) Phi
0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | eleq1d 2419 |
. . . 4
![(](lp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) Phi 0c![}](rbrace.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | df-proj2 4568 |
. . . 4
Proj2 ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![{](lbrace.gif) Phi 0c![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) ![}](rbrace.gif) |
27 | 4, 25, 26 | elab2 2988 |
. . 3
![(](lp.gif) Proj2 ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) Phi 0c![}](rbrace.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) ![)](rp.gif) |
28 | | 0cnelphi 4597 |
. . . . . . . 8
0c
Phi ![y](_y.gif) |
29 | | ssun2 3427 |
. . . . . . . . . 10
0c Phi 0c![}](rbrace.gif) ![)](rp.gif) |
30 | | 0cex 4392 |
. . . . . . . . . . 11
0c
![_V](rmcv.gif) |
31 | 30 | snid 3760 |
. . . . . . . . . 10
0c
0c![}](rbrace.gif) |
32 | 29, 31 | sselii 3270 |
. . . . . . . . 9
0c
Phi 0c![}](rbrace.gif) ![)](rp.gif) |
33 | | eleq2 2414 |
. . . . . . . . 9
![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c Phi 0c![}](rbrace.gif)
0c
Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 32, 33 | mpbii 202 |
. . . . . . . 8
![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi
0c
Phi ![y](_y.gif) ![)](rp.gif) |
35 | 28, 34 | mto 167 |
. . . . . . 7
Phi 0c![}](rbrace.gif)
Phi ![y](_y.gif) |
36 | 35 | a1i 10 |
. . . . . 6
![(](lp.gif) Phi 0c![}](rbrace.gif) Phi
![y](_y.gif) ![)](rp.gif) |
37 | 36 | nrex 2716 |
. . . . 5
![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![y](_y.gif) |
38 | 37 | biorfi 396 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | orcom 376 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif)
Phi ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 38, 39 | bitri 240 |
. . 3
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 22, 27, 40 | 3bitr4i 268 |
. 2
![(](lp.gif) Proj2 ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![B](_cb.gif) ![)](rp.gif) |
42 | 41 | eqriv 2350 |
1
Proj2 ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![B](_cb.gif) |