Proof of Theorem fnfreclem1
Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . 5
![_V](rmcv.gif) |
2 | 1 | elcompl 3225 |
. . . 4
![(](lp.gif) ∼
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![)](rp.gif) ![)](rp.gif) |
3 | | elrn2 4897 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![E.](exists.gif) ![y](_y.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![)](rp.gif) ![)](rp.gif) |
4 | | elrn2 4897 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![E.](exists.gif) ![z](_z.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![)](rp.gif) ![)](rp.gif) |
5 | | eldif 3221 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![>.](rangle.gif) Ins3 ![)](rp.gif) ![)](rp.gif) |
6 | | elin 3219 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | opelcnv 4893 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![`'](_cnv.gif) ![<.](langle.gif) ![w](_w.gif) ![y](_y.gif) ![F](_cf.gif) ![)](rp.gif) |
8 | | vex 2862 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
9 | | opelxp 4811 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![(](lp.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 8, 9 | mpbiran 884 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![)](rp.gif) |
11 | | df-br 4640 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![<.](langle.gif) ![w](_w.gif) ![y](_y.gif) ![F](_cf.gif) ![)](rp.gif) |
12 | 7, 10, 11 | 3bitr4i 268 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![y](_y.gif) ![)](rp.gif) |
13 | | opelcnv 4893 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![`'](_cnv.gif) ![<.](langle.gif) ![w](_w.gif) ![z](_z.gif) ![F](_cf.gif) ![)](rp.gif) |
14 | | vex 2862 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
15 | 14 | otelins2 5791 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins2 ![`'](_cnv.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![)](rp.gif) |
16 | | df-br 4640 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![<.](langle.gif) ![w](_w.gif) ![z](_z.gif) ![F](_cf.gif) ![)](rp.gif) |
17 | 13, 15, 16 | 3bitr4i 268 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins2 ![`'](_cnv.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) |
18 | 12, 17 | anbi12i 678 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif)
![(](lp.gif) ![w](_w.gif) ![F](_cf.gif)
![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 6, 18 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 1 | otelins3 5792 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins3 ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) |
21 | | df-br 4640 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![y](_y.gif) ![)](rp.gif) |
22 | 14 | ideq 4870 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![y](_y.gif) ![)](rp.gif) |
23 | | equcom 1680 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) |
24 | 22, 23 | bitri 240 |
. . . . . . . . . . . . 13
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) |
25 | 20, 21, 24 | 3bitr2i 264 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins3 ![z](_z.gif) ![)](rp.gif) |
26 | 25 | notbii 287 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) Ins3 ![z](_z.gif) ![)](rp.gif) |
27 | 19, 26 | anbi12i 678 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![>.](rangle.gif) Ins3 ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 5, 27 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | exbii 1582 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![<.](langle.gif) ![z](_z.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 4, 29 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![y](_y.gif)
![w](_w.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | exbii 1582 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![<.](langle.gif) ![y](_y.gif) ![w](_w.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | exanali 1585 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![E.](exists.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | exnal 1574 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 33, 34 | bitri 240 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 3, 31, 35 | 3bitrri 263 |
. . . . 5
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![)](rp.gif) ![)](rp.gif) |
37 | 36 | con1bii 321 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 2, 37 | bitri 240 |
. . 3
![(](lp.gif) ∼
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | abbi2i 2464 |
. 2
∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![{](lbrace.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![}](rbrace.gif) |
40 | | vvex 4109 |
. . . . . 6
![_V](rmcv.gif) |
41 | | cnvexg 5101 |
. . . . . 6
![(](lp.gif) ![`'](_cnv.gif)
![_V](rmcv.gif) ![)](rp.gif) |
42 | | xpexg 5114 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif)
![_V](rmcv.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![_V](rmcv.gif) ![)](rp.gif) |
43 | 40, 41, 42 | sylancr 644 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) ![_V](rmcv.gif) ![)](rp.gif) |
44 | | ins2exg 5795 |
. . . . . 6
![(](lp.gif) ![`'](_cnv.gif) Ins2
![`'](_cnv.gif) ![_V](rmcv.gif) ![)](rp.gif) |
45 | 41, 44 | syl 15 |
. . . . 5
![(](lp.gif) Ins2 ![`'](_cnv.gif) ![_V](rmcv.gif) ![)](rp.gif) |
46 | | inexg 4100 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![_V](rmcv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![_V](rmcv.gif) ![)](rp.gif) |
47 | 43, 45, 46 | syl2anc 642 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![_V](rmcv.gif) ![)](rp.gif) |
48 | | idex 5504 |
. . . . . 6
![_V](rmcv.gif) |
49 | 48 | ins3ex 5798 |
. . . . 5
Ins3 ![_V](rmcv.gif) |
50 | | difexg 4102 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
51 | 49, 50 | mpan2 652 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
52 | | rnexg 5104 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif)
Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
53 | 47, 51, 52 | 3syl 18 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
54 | | rnexg 5104 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
55 | | complexg 4099 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
56 | 53, 54, 55 | 3syl 18 |
. 2
![(](lp.gif) ∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![F](_cf.gif) Ins2 ![`'](_cnv.gif) ![F](_cf.gif) Ins3 ![_V](rmcv.gif) ![)](rp.gif) |
57 | 39, 56 | syl5eqelr 2438 |
1
![(](lp.gif) ![{](lbrace.gif)
![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![_V](rmcv.gif) ![)](rp.gif) |