Metamath Proof Explorer

Theorem inf3lem5

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-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 inf3lem5 
|- ( ( x =/= (/) /\ x C_ U. x ) -> ( ( A e. _om /\ B e. A ) -> ( F ` B ) C. ( F ` A ) ) )

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 elnn 
 |-  ( ( B e. A /\ A e. _om ) -> B e. _om )
6 5 ancoms 
 |-  ( ( A e. _om /\ B e. A ) -> B e. _om )
7 nnord 
 |-  ( A e. _om -> Ord A )
8 ordsucss 
 |-  ( Ord A -> ( B e. A -> suc B C_ A ) )
9 7 8 syl 
 |-  ( A e. _om -> ( B e. A -> suc B C_ A ) )
10 9 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( B e. A -> suc B C_ A ) )
11 peano2b 
 |-  ( B e. _om <-> suc B e. _om )
12 fveq2 
 |-  ( v = suc B -> ( F ` v ) = ( F ` suc B ) )
13 12 psseq2d 
 |-  ( v = suc B -> ( ( F ` B ) C. ( F ` v ) <-> ( F ` B ) C. ( F ` suc B ) ) )
14 13 imbi2d 
 |-  ( v = suc B -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` v ) ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` suc B ) ) ) )
15 fveq2 
 |-  ( v = u -> ( F ` v ) = ( F ` u ) )
16 15 psseq2d 
 |-  ( v = u -> ( ( F ` B ) C. ( F ` v ) <-> ( F ` B ) C. ( F ` u ) ) )
17 16 imbi2d 
 |-  ( v = u -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` v ) ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` u ) ) ) )
18 fveq2 
 |-  ( v = suc u -> ( F ` v ) = ( F ` suc u ) )
19 18 psseq2d 
 |-  ( v = suc u -> ( ( F ` B ) C. ( F ` v ) <-> ( F ` B ) C. ( F ` suc u ) ) )
20 19 imbi2d 
 |-  ( v = suc u -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` v ) ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` suc u ) ) ) )
21 fveq2 
 |-  ( v = A -> ( F ` v ) = ( F ` A ) )
22 21 psseq2d 
 |-  ( v = A -> ( ( F ` B ) C. ( F ` v ) <-> ( F ` B ) C. ( F ` A ) ) )
23 22 imbi2d 
 |-  ( v = A -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` v ) ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) ) )
24 1 2 4 4 inf3lem4 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( B e. _om -> ( F ` B ) C. ( F ` suc B ) ) )
25 24 com12 
 |-  ( B e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` suc B ) ) )
26 11 25 sylbir 
 |-  ( suc B e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` suc B ) ) )
27 vex 
 |-  u e. _V
28 1 2 27 4 inf3lem4 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( u e. _om -> ( F ` u ) C. ( F ` suc u ) ) )
29 psstr 
 |-  ( ( ( F ` B ) C. ( F ` u ) /\ ( F ` u ) C. ( F ` suc u ) ) -> ( F ` B ) C. ( F ` suc u ) )
30 29 expcom 
 |-  ( ( F ` u ) C. ( F ` suc u ) -> ( ( F ` B ) C. ( F ` u ) -> ( F ` B ) C. ( F ` suc u ) ) )
31 28 30 syl6com 
 |-  ( u e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( ( F ` B ) C. ( F ` u ) -> ( F ` B ) C. ( F ` suc u ) ) ) )
32 31 a2d 
 |-  ( u e. _om -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` u ) ) -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` suc u ) ) ) )
33 32 ad2antrr 
 |-  ( ( ( u e. _om /\ suc B e. _om ) /\ suc B C_ u ) -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` u ) ) -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` suc u ) ) ) )
34 14 17 20 23 26 33 findsg 
 |-  ( ( ( A e. _om /\ suc B e. _om ) /\ suc B C_ A ) -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) )
35 34 ex 
 |-  ( ( A e. _om /\ suc B e. _om ) -> ( suc B C_ A -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) ) )
36 11 35 sylan2b 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc B C_ A -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) ) )
37 10 36 syld 
 |-  ( ( A e. _om /\ B e. _om ) -> ( B e. A -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) ) )
38 37 impancom 
 |-  ( ( A e. _om /\ B e. A ) -> ( B e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) ) )
39 6 38 mpd 
 |-  ( ( A e. _om /\ B e. A ) -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` B ) C. ( F ` A ) ) )
40 39 com12 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( ( A e. _om /\ B e. A ) -> ( F ` B ) C. ( F ` A ) ) )