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