Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rpnnen2.1 | |
|
Assertion | rpnnen2lem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpnnen2.1 | |
|
2 | nnex | |
|
3 | 2 | elpw2 | |
4 | eleq2 | |
|
5 | 4 | ifbid | |
6 | 5 | mpteq2dv | |
7 | 2 | mptex | |
8 | 6 1 7 | fvmpt | |
9 | 3 8 | sylbir | |
10 | 9 | fveq1d | |
11 | eleq1 | |
|
12 | oveq2 | |
|
13 | 11 12 | ifbieq1d | |
14 | eqid | |
|
15 | ovex | |
|
16 | c0ex | |
|
17 | 15 16 | ifex | |
18 | 13 14 17 | fvmpt | |
19 | 10 18 | sylan9eq | |