Metamath Proof Explorer


Theorem rpnnen2lem1

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

Ref Expression
Hypothesis rpnnen2.1 F=x𝒫nifnx13n0
Assertion rpnnen2lem1 ANFAN=ifNA13N0

Proof

Step Hyp Ref Expression
1 rpnnen2.1 F=x𝒫nifnx13n0
2 nnex V
3 2 elpw2 A𝒫A
4 eleq2 x=AnxnA
5 4 ifbid x=Aifnx13n0=ifnA13n0
6 5 mpteq2dv x=Anifnx13n0=nifnA13n0
7 2 mptex nifnA13n0V
8 6 1 7 fvmpt A𝒫FA=nifnA13n0
9 3 8 sylbir AFA=nifnA13n0
10 9 fveq1d AFAN=nifnA13n0N
11 eleq1 n=NnANA
12 oveq2 n=N13n=13N
13 11 12 ifbieq1d n=NifnA13n0=ifNA13N0
14 eqid nifnA13n0=nifnA13n0
15 ovex 13NV
16 c0ex 0V
17 15 16 ifex ifNA13N0V
18 13 14 17 fvmpt NnifnA13n0N=ifNA13N0
19 10 18 sylan9eq ANFAN=ifNA13N0