Step | Hyp | Ref
| Expression |
1 | | df-pw1fn 5766 |
. . 3
Pw1Fn ![(](lp.gif) 1c 1 ![U.](bigcup.gif) ![x](_x.gif) ![)](rp.gif) |
2 | | oteltxp 5782 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) SI S
S ![)](rp.gif) 1c![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) SI
S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | snex 4111 |
. . . . . . . . . . 11
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
4 | 3 | ideq 4870 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
5 | | df-br 4640 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
6 | | eqcom 2355 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![y](_y.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
7 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
8 | 7 | sneqb 3876 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) |
9 | 6, 8 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) |
10 | 4, 5, 9 | 3bitr3i 266 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) |
11 | | oteltxp 5782 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) SI S S ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) SI
S ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) S ![)](rp.gif) ![)](rp.gif) |
12 | | snex 4111 |
. . . . . . . . . . . . . . 15
![{](lbrace.gif) ![t](_t.gif)
![_V](rmcv.gif) |
13 | 7, 12 | brsnsi 5773 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) SI S ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![y](_y.gif) S ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) |
14 | | df-br 4640 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) SI S ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) SI
S ![)](rp.gif) |
15 | | brcnv 4892 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![y](_y.gif) S ![{](lbrace.gif) ![t](_t.gif) ![{](lbrace.gif) ![t](_t.gif) S ![y](_y.gif) ![)](rp.gif) |
16 | | vex 2862 |
. . . . . . . . . . . . . . . 16
![_V](rmcv.gif) |
17 | 16, 7 | brssetsn 4759 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![t](_t.gif) S ![y](_y.gif) ![)](rp.gif) |
18 | 15, 17 | bitri 240 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![y](_y.gif) S ![{](lbrace.gif) ![t](_t.gif) ![y](_y.gif) ![)](rp.gif) |
19 | 13, 14, 18 | 3bitr3i 266 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) SI S ![y](_y.gif) ![)](rp.gif) |
20 | | vex 2862 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
21 | 7, 20 | opelssetsn 4760 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) S ![x](_x.gif) ![)](rp.gif) |
22 | 19, 21 | anbi12i 678 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) SI S ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) S ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 11, 22 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) SI S S ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | exbii 1582 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) SI S S ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | elima1c 4947 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c ![E.](exists.gif) ![y](_y.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) SI S S ![)](rp.gif) ![)](rp.gif) |
26 | | eluni 3894 |
. . . . . . . . . 10
![(](lp.gif) ![U.](bigcup.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 24, 25, 26 | 3bitr4i 268 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c ![U.](bigcup.gif) ![x](_x.gif) ![)](rp.gif) |
28 | 10, 27 | anbi12i 678 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![t](_t.gif)
![U.](bigcup.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 2, 28 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) SI S
S ![)](rp.gif) 1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![t](_t.gif)
![U.](bigcup.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | ancom 437 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![t](_t.gif) ![U.](bigcup.gif) ![x](_x.gif)
![(](lp.gif) ![U.](bigcup.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 29, 30 | bitri 240 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) SI S
S ![)](rp.gif) 1c![)](rp.gif) ![(](lp.gif) ![U.](bigcup.gif)
![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 31 | exbii 1582 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![>.](rangle.gif)
![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![U.](bigcup.gif)
![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | elimapw11c 4948 |
. . . . 5
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) !["](backquote.gif) 1 1c ![E.](exists.gif) ![t](_t.gif) ![<.](langle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | elpw1 4144 |
. . . . . 6
![(](lp.gif) 1 ![U.](bigcup.gif) ![E.](exists.gif) ![U.](bigcup.gif) ![x](_x.gif) ![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) |
35 | | df-rex 2620 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
![U.](bigcup.gif) ![x](_x.gif)
![{](lbrace.gif) ![t](_t.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![U.](bigcup.gif)
![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 34, 35 | bitri 240 |
. . . . 5
![(](lp.gif) 1 ![U.](bigcup.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![U.](bigcup.gif)
![{](lbrace.gif) ![t](_t.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 32, 33, 36 | 3bitr4i 268 |
. . . 4
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) !["](backquote.gif) 1 1c 1 ![U.](bigcup.gif) ![x](_x.gif) ![)](rp.gif) |
38 | 37 | releqmpt 5808 |
. . 3
![(](lp.gif) 1c ![_V](rmcv.gif)
∼ ![(](lp.gif) Ins3 S
Ins2 ![(](lp.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) !["](backquote.gif) 1 1c![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif)
![(](lp.gif)
1c 1 ![U.](bigcup.gif) ![x](_x.gif) ![)](rp.gif) |
39 | 1, 38 | eqtr4i 2376 |
. 2
Pw1Fn ![(](lp.gif) 1c ![_V](rmcv.gif) ∼
![(](lp.gif) Ins3 S Ins2 ![(](lp.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) !["](backquote.gif) 1 1c![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
40 | | 1cex 4142 |
. . 3
1c
![_V](rmcv.gif) |
41 | | idex 5504 |
. . . . 5
![_V](rmcv.gif) |
42 | | ssetex 4744 |
. . . . . . . . 9
S ![_V](rmcv.gif) |
43 | 42 | cnvex 5102 |
. . . . . . . 8
S
![_V](rmcv.gif) |
44 | 43 | siex 4753 |
. . . . . . 7
SI S ![_V](rmcv.gif) |
45 | 44, 42 | txpex 5785 |
. . . . . 6
SI
S S
![_V](rmcv.gif) |
46 | 45, 40 | imaex 4747 |
. . . . 5
![(](lp.gif) SI S
S ![)](rp.gif) 1c ![_V](rmcv.gif) |
47 | 41, 46 | txpex 5785 |
. . . 4
![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif)
![_V](rmcv.gif) |
48 | 40 | pw1ex 4303 |
. . . 4
1
1c
![_V](rmcv.gif) |
49 | 47, 48 | imaex 4747 |
. . 3
![(](lp.gif) ![(](lp.gif) SI S
S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) !["](backquote.gif) 1 1c ![_V](rmcv.gif) |
50 | 40, 49 | mptexlem 5810 |
. 2
![(](lp.gif) 1c ![_V](rmcv.gif)
∼ ![(](lp.gif) Ins3 S
Ins2 ![(](lp.gif) ![(](lp.gif) SI S S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) !["](backquote.gif) 1 1c![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif)
![_V](rmcv.gif) |
51 | 39, 50 | eqeltri 2423 |
1
Pw1Fn ![_V](rmcv.gif) |