Step | Hyp | Ref
| Expression |
1 | | df-ranfn 5772 |
. . 3
Ran ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) |
2 | | elin 3219 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4 SI3 Ins2 Ins2 S ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4
SI3 ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins2
Ins2 S ![)](rp.gif) ![)](rp.gif) |
3 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
4 | 3 | oqelins4 5794 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4 SI3
![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif)
![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>.](rangle.gif) SI3 ![)](rp.gif) |
5 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
6 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
7 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
8 | 5, 6, 7 | otsnelsi3 5805 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>.](rangle.gif) SI3 ![<.](langle.gif) ![w](_w.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
9 | | df-br 4640 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![<.](langle.gif) ![w](_w.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
10 | 6, 7 | opex 4588 |
. . . . . . . . . . . . 13
![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![_V](rmcv.gif) |
11 | 10 | ideq 4870 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
12 | 8, 9, 11 | 3bitr2i 264 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>.](rangle.gif) SI3
![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
13 | 4, 12 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4 SI3
![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) |
14 | | snex 4111 |
. . . . . . . . . . . 12
![{](lbrace.gif) ![z](_z.gif)
![_V](rmcv.gif) |
15 | 14 | otelins2 5791 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins2 Ins2 S ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) Ins2 S ![)](rp.gif) |
16 | | snex 4111 |
. . . . . . . . . . . . 13
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
17 | 16 | otelins2 5791 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) Ins2 S ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif)
![x](_x.gif) S ![)](rp.gif) |
18 | 5, 3 | opelssetsn 4760 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![x](_x.gif) S ![x](_x.gif) ![)](rp.gif) |
19 | 17, 18 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) Ins2 S ![x](_x.gif) ![)](rp.gif) |
20 | 15, 19 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins2 Ins2 S ![x](_x.gif) ![)](rp.gif) |
21 | 13, 20 | anbi12i 678 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4
SI3 ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins2
Ins2 S ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 2, 21 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4 SI3 Ins2 Ins2 S ![(](lp.gif)
![<.](langle.gif) ![z](_z.gif)
![y](_y.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4 SI3 Ins2 Ins2 S ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | elima1c 4947 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c ![E.](exists.gif) ![w](_w.gif) ![<.](langle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif)
![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![>.](rangle.gif) ![>.](rangle.gif) Ins4 SI3
Ins2
Ins2 S ![)](rp.gif) ![)](rp.gif) |
25 | | df-clel 2349 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![y](_y.gif)
![E.](exists.gif) ![w](_w.gif) ![(](lp.gif)
![<.](langle.gif) ![z](_z.gif)
![y](_y.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 23, 24, 25 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![x](_x.gif) ![)](rp.gif) |
27 | 26 | exbii 1582 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif)
Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c ![E.](exists.gif) ![z](_z.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![x](_x.gif) ![)](rp.gif) |
28 | | elima1c 4947 |
. . . . 5
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c![)](rp.gif) 1c ![E.](exists.gif) ![z](_z.gif) ![<.](langle.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![>.](rangle.gif) ![(](lp.gif) Ins4 SI3
Ins2
Ins2 S ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
29 | | elrn2 4897 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![x](_x.gif) ![)](rp.gif) |
30 | 27, 28, 29 | 3bitr4i 268 |
. . . 4
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c![)](rp.gif) 1c ![x](_x.gif) ![)](rp.gif) |
31 | 30 | releqmpt 5808 |
. . 3
![(](lp.gif) ![(](lp.gif) ![_V](rmcv.gif) ∼ ![(](lp.gif) Ins3 S Ins2 ![(](lp.gif) ![(](lp.gif) Ins4 SI3
Ins2
Ins2 S ![)](rp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) |
32 | 1, 31 | eqtr4i 2376 |
. 2
Ran ![(](lp.gif) ![(](lp.gif) ![_V](rmcv.gif) ∼ ![(](lp.gif) Ins3 S
Ins2 ![(](lp.gif) ![(](lp.gif) Ins4 SI3
Ins2
Ins2 S ![)](rp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
33 | | vvex 4109 |
. . 3
![_V](rmcv.gif) |
34 | | idex 5504 |
. . . . . . . 8
![_V](rmcv.gif) |
35 | 34 | si3ex 5806 |
. . . . . . 7
SI3 ![_V](rmcv.gif) |
36 | 35 | ins4ex 5799 |
. . . . . 6
Ins4 SI3
![_V](rmcv.gif) |
37 | | ssetex 4744 |
. . . . . . . 8
S ![_V](rmcv.gif) |
38 | 37 | ins2ex 5797 |
. . . . . . 7
Ins2 S ![_V](rmcv.gif) |
39 | 38 | ins2ex 5797 |
. . . . . 6
Ins2 Ins2 S ![_V](rmcv.gif) |
40 | 36, 39 | inex 4105 |
. . . . 5
Ins4 SI3
Ins2
Ins2 S ![_V](rmcv.gif) |
41 | | 1cex 4142 |
. . . . 5
1c
![_V](rmcv.gif) |
42 | 40, 41 | imaex 4747 |
. . . 4
![(](lp.gif) Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c ![_V](rmcv.gif) |
43 | 42, 41 | imaex 4747 |
. . 3
![(](lp.gif) ![(](lp.gif) Ins4 SI3 Ins2 Ins2 S ![)](rp.gif) 1c![)](rp.gif) 1c
![_V](rmcv.gif) |
44 | 33, 43 | mptexlem 5810 |
. 2
![(](lp.gif) ![(](lp.gif) ![_V](rmcv.gif) ∼ ![(](lp.gif) Ins3 S Ins2 ![(](lp.gif) ![(](lp.gif) Ins4 SI3
Ins2
Ins2 S ![)](rp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![_V](rmcv.gif) |
45 | 32, 44 | eqeltri 2423 |
1
Ran ![_V](rmcv.gif) |