Metamath Proof Explorer


Theorem inf3lemd

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 G = y V w x | w x y
inf3lem.2 F = rec G ω
inf3lem.3 A V
inf3lem.4 B V
Assertion inf3lemd A ω F A x

Proof

Step Hyp Ref Expression
1 inf3lem.1 G = y V w x | w x y
2 inf3lem.2 F = rec G ω
3 inf3lem.3 A V
4 inf3lem.4 B V
5 fveq2 A = F A = F
6 1 2 3 4 inf3lemb F =
7 5 6 eqtrdi A = F A =
8 0ss x
9 7 8 eqsstrdi A = F A x
10 9 a1d A = A ω F A x
11 nnsuc A ω A v ω A = suc v
12 vex v V
13 1 2 12 4 inf3lemc v ω F suc v = G F v
14 13 eleq2d v ω u F suc v u G F v
15 vex u V
16 fvex F v V
17 1 2 15 16 inf3lema u G F v u x u x F v
18 17 simplbi u G F v u x
19 14 18 syl6bi v ω u F suc v u x
20 19 ssrdv v ω F suc v x
21 fveq2 A = suc v F A = F suc v
22 21 sseq1d A = suc v F A x F suc v x
23 20 22 syl5ibrcom v ω A = suc v F A x
24 23 rexlimiv v ω A = suc v F A x
25 11 24 syl A ω A F A x
26 25 expcom A A ω F A x
27 10 26 pm2.61ine A ω F A x