Step | Hyp | Ref
| Expression |
1 | | pw1fnf1o 5855 |
. . . . 5
Pw1Fn 1c![-1-1-onto->](onetooneonto.gif) 1c |
2 | | f1of1 5286 |
. . . . 5
Pw1Fn 1c![-1-1-onto->](onetooneonto.gif) 1c Pw1Fn 1c![-1-1->](onetoone.gif) 1c![)](rp.gif) |
3 | 1, 2 | ax-mp 5 |
. . . 4
Pw1Fn 1c![-1-1->](onetoone.gif) 1c |
4 | | pw1ss1c 4158 |
. . . 4
1 ![~P](scrp.gif) 1c |
5 | | f1ores 5300 |
. . . 4
![(](lp.gif) Pw1Fn 1c![-1-1->](onetoone.gif) 1c
1 ![~P](scrp.gif) 1c Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 3, 4, 5 | mp2an 653 |
. . 3
Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) |
7 | | df-ima 4727 |
. . . . 5
Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![{](lbrace.gif)
![E.](exists.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn ![x](_x.gif) ![}](rbrace.gif) |
8 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
9 | 8 | elpw 3728 |
. . . . . . . 8
![(](lp.gif) ![~P](scrp.gif) 1 1 ![A](_ca.gif) ![)](rp.gif) |
10 | 8 | sspw1 4335 |
. . . . . . . 8
![(](lp.gif) 1 ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif)
1 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | df-rex 2620 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
![A](_ca.gif)
1 ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif)
![~P](scrp.gif) 1 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | df-pw 3724 |
. . . . . . . . . . . 12
![~P](scrp.gif) ![{](lbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) |
13 | 12 | abeq2i 2460 |
. . . . . . . . . . 11
![(](lp.gif) ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) |
14 | 13 | anbi1i 676 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![~P](scrp.gif)
1 ![z](_z.gif) ![(](lp.gif) 1 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 14 | exbii 1582 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![~P](scrp.gif) 1 ![z](_z.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif)
1 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 11, 15 | bitr2i 241 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif)
1 ![z](_z.gif) ![E.](exists.gif) ![A](_ca.gif) 1 ![z](_z.gif) ![)](rp.gif) |
17 | 9, 10, 16 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) ![~P](scrp.gif) 1 ![E.](exists.gif) ![A](_ca.gif) 1 ![z](_z.gif) ![)](rp.gif) |
18 | | df-rex 2620 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif)
1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) 1 ![~P](scrp.gif)
Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | elpw1 4144 |
. . . . . . . . . . 11
![(](lp.gif) 1 ![~P](scrp.gif) ![E.](exists.gif) ![A](_ca.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) |
20 | 19 | anbi1i 676 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1 ![~P](scrp.gif)
Pw1Fn ![x](_x.gif)
![(](lp.gif) ![E.](exists.gif)
![A](_ca.gif)
![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | r19.41v 2764 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif)
![A](_ca.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif)
![A](_ca.gif)
![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 20, 21 | bitr4i 243 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1 ![~P](scrp.gif)
Pw1Fn ![x](_x.gif)
![E.](exists.gif) ![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif)
Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | exbii 1582 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) 1 ![~P](scrp.gif) Pw1Fn ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif)
![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | rexcom4 2878 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
![A](_ca.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif)
Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | snex 4111 |
. . . . . . . . . . . 12
![{](lbrace.gif) ![z](_z.gif)
![_V](rmcv.gif) |
26 | | breq1 4642 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) Pw1Fn ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 25, 26 | ceqsexv 2894 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![)](rp.gif) |
28 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
29 | 28 | brpw1fn 5854 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn 1 ![z](_z.gif) ![)](rp.gif) |
30 | 27, 29 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) 1 ![z](_z.gif) ![)](rp.gif) |
31 | 30 | rexbii 2639 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
![A](_ca.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![E.](exists.gif) ![A](_ca.gif)
1 ![z](_z.gif) ![)](rp.gif) |
32 | 24, 31 | bitr3i 242 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) Pw1Fn ![x](_x.gif) ![E.](exists.gif) ![A](_ca.gif) 1 ![z](_z.gif) ![)](rp.gif) |
33 | 18, 23, 32 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn ![E.](exists.gif)
![A](_ca.gif)
1 ![z](_z.gif) ![)](rp.gif) |
34 | 17, 33 | bitr4i 243 |
. . . . . 6
![(](lp.gif) ![~P](scrp.gif) 1 ![E.](exists.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn ![x](_x.gif) ![)](rp.gif) |
35 | 34 | abbi2i 2464 |
. . . . 5
![~P](scrp.gif) 1 ![{](lbrace.gif) ![E.](exists.gif)
1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn ![x](_x.gif) ![}](rbrace.gif) |
36 | 7, 35 | eqtr4i 2376 |
. . . 4
Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![~P](scrp.gif) 1 ![A](_ca.gif) |
37 | | f1oeq3 5283 |
. . . 4
![(](lp.gif) Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif)
![~P](scrp.gif) 1 ![(](lp.gif) Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![~P](scrp.gif) 1 ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 36, 37 | ax-mp 5 |
. . 3
![(](lp.gif) Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) Pw1Fn !["](backquote.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![~P](scrp.gif) 1 ![A](_ca.gif) ![)](rp.gif) |
39 | 6, 38 | mpbi 199 |
. 2
Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![~P](scrp.gif) 1 ![A](_ca.gif) |
40 | | pw1fnex 5852 |
. . . 4
Pw1Fn ![_V](rmcv.gif) |
41 | | enpw1pw.1 |
. . . . . 6
![_V](rmcv.gif) |
42 | 41 | pwex 4329 |
. . . . 5
![~P](scrp.gif) ![_V](rmcv.gif) |
43 | 42 | pw1ex 4303 |
. . . 4
1 ![~P](scrp.gif) ![_V](rmcv.gif) |
44 | 40, 43 | resex 5117 |
. . 3
Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![_V](rmcv.gif) |
45 | 44 | f1oen 6033 |
. 2
![(](lp.gif) Pw1Fn 1 ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) 1 ![~P](scrp.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![~P](scrp.gif) 1 1 ![~P](scrp.gif) ![~P](scrp.gif) 1 ![A](_ca.gif) ![)](rp.gif) |
46 | 39, 45 | ax-mp 5 |
1
1 ![~P](scrp.gif) ![~P](scrp.gif) 1 ![A](_ca.gif) |