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 e. _V |-> { w e. x | ( w i^i x ) C_ y } )
inf3lem.2
|- F = ( rec ( G , (/) ) |` _om )
inf3lem.3
|- A e. _V
inf3lem.4
|- B e. _V
Assertion inf3lemd
|- ( A e. _om -> ( F ` A ) C_ x )

Proof

Step Hyp Ref Expression
1 inf3lem.1
 |-  G = ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } )
2 inf3lem.2
 |-  F = ( rec ( G , (/) ) |` _om )
3 inf3lem.3
 |-  A e. _V
4 inf3lem.4
 |-  B e. _V
5 fveq2
 |-  ( A = (/) -> ( F ` A ) = ( F ` (/) ) )
6 1 2 3 4 inf3lemb
 |-  ( F ` (/) ) = (/)
7 5 6 eqtrdi
 |-  ( A = (/) -> ( F ` A ) = (/) )
8 0ss
 |-  (/) C_ x
9 7 8 eqsstrdi
 |-  ( A = (/) -> ( F ` A ) C_ x )
10 9 a1d
 |-  ( A = (/) -> ( A e. _om -> ( F ` A ) C_ x ) )
11 nnsuc
 |-  ( ( A e. _om /\ A =/= (/) ) -> E. v e. _om A = suc v )
12 vex
 |-  v e. _V
13 1 2 12 4 inf3lemc
 |-  ( v e. _om -> ( F ` suc v ) = ( G ` ( F ` v ) ) )
14 13 eleq2d
 |-  ( v e. _om -> ( u e. ( F ` suc v ) <-> u e. ( G ` ( F ` v ) ) ) )
15 vex
 |-  u e. _V
16 fvex
 |-  ( F ` v ) e. _V
17 1 2 15 16 inf3lema
 |-  ( u e. ( G ` ( F ` v ) ) <-> ( u e. x /\ ( u i^i x ) C_ ( F ` v ) ) )
18 17 simplbi
 |-  ( u e. ( G ` ( F ` v ) ) -> u e. x )
19 14 18 syl6bi
 |-  ( v e. _om -> ( u e. ( F ` suc v ) -> u e. x ) )
20 19 ssrdv
 |-  ( v e. _om -> ( F ` suc v ) C_ x )
21 fveq2
 |-  ( A = suc v -> ( F ` A ) = ( F ` suc v ) )
22 21 sseq1d
 |-  ( A = suc v -> ( ( F ` A ) C_ x <-> ( F ` suc v ) C_ x ) )
23 20 22 syl5ibrcom
 |-  ( v e. _om -> ( A = suc v -> ( F ` A ) C_ x ) )
24 23 rexlimiv
 |-  ( E. v e. _om A = suc v -> ( F ` A ) C_ x )
25 11 24 syl
 |-  ( ( A e. _om /\ A =/= (/) ) -> ( F ` A ) C_ x )
26 25 expcom
 |-  ( A =/= (/) -> ( A e. _om -> ( F ` A ) C_ x ) )
27 10 26 pm2.61ine
 |-  ( A e. _om -> ( F ` A ) C_ x )