Step | Hyp | Ref
| Expression |
1 | | eleq1 2200 |
. 2
Omni Omni |
2 | | eleq1 2200 |
. 2
Omni
Omni |
3 | | eleq1 2200 |
. 2
Omni Omni |
4 | | eleq1 2200 |
. 2
Omni
Omni |
5 | | 0ex 4050 |
. . . 4
|
6 | | isomni 7001 |
. . . 4
Omni
|
7 | 5, 6 | ax-mp 5 |
. . 3
Omni
|
8 | | ral0 3459 |
. . . . 5
|
9 | 8 | olci 721 |
. . . 4
|
10 | 9 | a1i 9 |
. . 3
|
11 | 7, 10 | mpgbir 1429 |
. 2
Omni |
12 | | elun1 3238 |
. . . . . . . . . . . 12
|
13 | 12 | ad2antlr 480 |
. . . . . . . . . . 11
Omni |
14 | | fvres 5438 |
. . . . . . . . . . . . 13
|
15 | 14 | ad2antlr 480 |
. . . . . . . . . . . 12
Omni |
16 | | simpr 109 |
. . . . . . . . . . . 12
Omni |
17 | 15, 16 | eqtr3d 2172 |
. . . . . . . . . . 11
Omni |
18 | | fveq2 5414 |
. . . . . . . . . . . . 13
|
19 | 18 | eqeq1d 2146 |
. . . . . . . . . . . 12
|
20 | 19 | rspcev 2784 |
. . . . . . . . . . 11
|
21 | 13, 17, 20 | syl2anc 408 |
. . . . . . . . . 10
Omni |
22 | 21 | orcd 722 |
. . . . . . . . 9
Omni
|
23 | 22 | ex 114 |
. . . . . . . 8
Omni
|
24 | 23 | rexlimdva 2547 |
. . . . . . 7
Omni
|
25 | | vsnid 3552 |
. . . . . . . . . . . . 13
|
26 | | elun2 3239 |
. . . . . . . . . . . . 13
|
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
|
28 | 27 | a1i 9 |
. . . . . . . . . . 11
Omni |
29 | | fveq2 5414 |
. . . . . . . . . . . . 13
|
30 | 29 | eqeq1d 2146 |
. . . . . . . . . . . 12
|
31 | 30 | rspcev 2784 |
. . . . . . . . . . 11
|
32 | 28, 31 | sylan 281 |
. . . . . . . . . 10
Omni |
33 | 32 | orcd 722 |
. . . . . . . . 9
Omni
|
34 | 33 | a1d 22 |
. . . . . . . 8
Omni
|
35 | | simpr 109 |
. . . . . . . . . . . 12
Omni
|
36 | | fveq2 5414 |
. . . . . . . . . . . . . . 15
|
37 | 36 | eqeq1d 2146 |
. . . . . . . . . . . . . 14
|
38 | 37 | cbvralv 2652 |
. . . . . . . . . . . . 13
|
39 | | fvres 5438 |
. . . . . . . . . . . . . . 15
|
40 | 39 | eqeq1d 2146 |
. . . . . . . . . . . . . 14
|
41 | 40 | ralbiia 2447 |
. . . . . . . . . . . . 13
|
42 | 38, 41 | bitri 183 |
. . . . . . . . . . . 12
|
43 | 35, 42 | sylib 121 |
. . . . . . . . . . 11
Omni
|
44 | | simplr 519 |
. . . . . . . . . . . 12
Omni
|
45 | | vex 2684 |
. . . . . . . . . . . . 13
|
46 | 29 | eqeq1d 2146 |
. . . . . . . . . . . . 13
|
47 | 45, 46 | ralsn 3562 |
. . . . . . . . . . . 12
|
48 | 44, 47 | sylibr 133 |
. . . . . . . . . . 11
Omni
|
49 | | ralun 3253 |
. . . . . . . . . . 11
|
50 | 43, 48, 49 | syl2anc 408 |
. . . . . . . . . 10
Omni
|
51 | 50 | olcd 723 |
. . . . . . . . 9
Omni
|
52 | 51 | ex 114 |
. . . . . . . 8
Omni
|
53 | | simpr 109 |
. . . . . . . . . . 11
Omni |
54 | 53, 28 | ffvelrnd 5549 |
. . . . . . . . . 10
Omni |
55 | | df2o3 6320 |
. . . . . . . . . 10
|
56 | 54, 55 | eleqtrdi 2230 |
. . . . . . . . 9
Omni |
57 | | elpri 3545 |
. . . . . . . . 9
|
58 | 56, 57 | syl 14 |
. . . . . . . 8
Omni |
59 | 34, 52, 58 | mpjaodan 787 |
. . . . . . 7
Omni
|
60 | | vex 2684 |
. . . . . . . . . . . 12
|
61 | | isomni 7001 |
. . . . . . . . . . . 12
Omni
|
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . 11
Omni
|
63 | 62 | biimpi 119 |
. . . . . . . . . 10
Omni
|
64 | 63 | adantl 275 |
. . . . . . . . 9
Omni
|
65 | | vex 2684 |
. . . . . . . . . . 11
|
66 | 65 | resex 4855 |
. . . . . . . . . 10
|
67 | | feq1 5250 |
. . . . . . . . . . 11
|
68 | | fveq1 5413 |
. . . . . . . . . . . . . 14
|
69 | 68 | eqeq1d 2146 |
. . . . . . . . . . . . 13
|
70 | 69 | rexbidv 2436 |
. . . . . . . . . . . 12
|
71 | 68 | eqeq1d 2146 |
. . . . . . . . . . . . 13
|
72 | 71 | ralbidv 2435 |
. . . . . . . . . . . 12
|
73 | 70, 72 | orbi12d 782 |
. . . . . . . . . . 11
|
74 | 67, 73 | imbi12d 233 |
. . . . . . . . . 10
|
75 | 66, 74 | spcv 2774 |
. . . . . . . . 9
|
76 | 64, 75 | syl 14 |
. . . . . . . 8
Omni
|
77 | | ssun1 3234 |
. . . . . . . . 9
|
78 | | fssres 5293 |
. . . . . . . . 9
|
79 | 77, 78 | mpan2 421 |
. . . . . . . 8
|
80 | 76, 79 | impel 278 |
. . . . . . 7
Omni
|
81 | 24, 59, 80 | mpjaod 707 |
. . . . . 6
Omni
|
82 | 81 | ex 114 |
. . . . 5
Omni
|
83 | 82 | alrimiv 1846 |
. . . 4
Omni
|
84 | 45 | snex 4104 |
. . . . . 6
|
85 | 60, 84 | unex 4357 |
. . . . 5
|
86 | | isomni 7001 |
. . . . 5
Omni
|
87 | 85, 86 | ax-mp 5 |
. . . 4
Omni
|
88 | 83, 87 | sylibr 133 |
. . 3
Omni Omni |
89 | 88 | ex 114 |
. 2
Omni
Omni |
90 | 1, 2, 3, 4, 11, 89 | findcard2 6776 |
1
Omni |