Metamath Proof Explorer

Theorem inf3lem3

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg . (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 inf3lem3 
|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= ( F ` suc 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 1 2 3 4 inf3lemd 
 |-  ( A e. _om -> ( F ` A ) C_ x )
6 1 2 3 4 inf3lem2 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= x ) )
7 6 com12 
 |-  ( A e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` A ) =/= x ) )
8 pssdifn0 
 |-  ( ( ( F ` A ) C_ x /\ ( F ` A ) =/= x ) -> ( x \ ( F ` A ) ) =/= (/) )
9 5 7 8 syl6an 
 |-  ( A e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( x \ ( F ` A ) ) =/= (/) ) )
10 vex 
 |-  x e. _V
11 10 difexi 
 |-  ( x \ ( F ` A ) ) e. _V
12 zfreg 
 |-  ( ( ( x \ ( F ` A ) ) e. _V /\ ( x \ ( F ` A ) ) =/= (/) ) -> E. v e. ( x \ ( F ` A ) ) ( v i^i ( x \ ( F ` A ) ) ) = (/) )
13 11 12 mpan 
 |-  ( ( x \ ( F ` A ) ) =/= (/) -> E. v e. ( x \ ( F ` A ) ) ( v i^i ( x \ ( F ` A ) ) ) = (/) )
14 eldifi 
 |-  ( v e. ( x \ ( F ` A ) ) -> v e. x )
15 inssdif0 
 |-  ( ( v i^i x ) C_ ( F ` A ) <-> ( v i^i ( x \ ( F ` A ) ) ) = (/) )
16 15 biimpri 
 |-  ( ( v i^i ( x \ ( F ` A ) ) ) = (/) -> ( v i^i x ) C_ ( F ` A ) )
17 14 16 anim12i 
 |-  ( ( v e. ( x \ ( F ` A ) ) /\ ( v i^i ( x \ ( F ` A ) ) ) = (/) ) -> ( v e. x /\ ( v i^i x ) C_ ( F ` A ) ) )
18 vex 
 |-  v e. _V
19 fvex 
 |-  ( F ` A ) e. _V
20 1 2 18 19 inf3lema 
 |-  ( v e. ( G ` ( F ` A ) ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` A ) ) )
21 17 20 sylibr 
 |-  ( ( v e. ( x \ ( F ` A ) ) /\ ( v i^i ( x \ ( F ` A ) ) ) = (/) ) -> v e. ( G ` ( F ` A ) ) )
22 1 2 3 4 inf3lemc 
 |-  ( A e. _om -> ( F ` suc A ) = ( G ` ( F ` A ) ) )
23 22 eleq2d 
 |-  ( A e. _om -> ( v e. ( F ` suc A ) <-> v e. ( G ` ( F ` A ) ) ) )
24 21 23 syl5ibr 
 |-  ( A e. _om -> ( ( v e. ( x \ ( F ` A ) ) /\ ( v i^i ( x \ ( F ` A ) ) ) = (/) ) -> v e. ( F ` suc A ) ) )
25 eldifn 
 |-  ( v e. ( x \ ( F ` A ) ) -> -. v e. ( F ` A ) )
26 25 adantr 
 |-  ( ( v e. ( x \ ( F ` A ) ) /\ ( v i^i ( x \ ( F ` A ) ) ) = (/) ) -> -. v e. ( F ` A ) )
27 24 26 jca2 
 |-  ( A e. _om -> ( ( v e. ( x \ ( F ` A ) ) /\ ( v i^i ( x \ ( F ` A ) ) ) = (/) ) -> ( v e. ( F ` suc A ) /\ -. v e. ( F ` A ) ) ) )
28 eleq2 
 |-  ( ( F ` A ) = ( F ` suc A ) -> ( v e. ( F ` A ) <-> v e. ( F ` suc A ) ) )
29 28 biimprd 
 |-  ( ( F ` A ) = ( F ` suc A ) -> ( v e. ( F ` suc A ) -> v e. ( F ` A ) ) )
30 iman 
 |-  ( ( v e. ( F ` suc A ) -> v e. ( F ` A ) ) <-> -. ( v e. ( F ` suc A ) /\ -. v e. ( F ` A ) ) )
31 29 30 sylib 
 |-  ( ( F ` A ) = ( F ` suc A ) -> -. ( v e. ( F ` suc A ) /\ -. v e. ( F ` A ) ) )
32 31 necon2ai 
 |-  ( ( v e. ( F ` suc A ) /\ -. v e. ( F ` A ) ) -> ( F ` A ) =/= ( F ` suc A ) )
33 27 32 syl6 
 |-  ( A e. _om -> ( ( v e. ( x \ ( F ` A ) ) /\ ( v i^i ( x \ ( F ` A ) ) ) = (/) ) -> ( F ` A ) =/= ( F ` suc A ) ) )
34 33 expd 
 |-  ( A e. _om -> ( v e. ( x \ ( F ` A ) ) -> ( ( v i^i ( x \ ( F ` A ) ) ) = (/) -> ( F ` A ) =/= ( F ` suc A ) ) ) )
35 34 rexlimdv 
 |-  ( A e. _om -> ( E. v e. ( x \ ( F ` A ) ) ( v i^i ( x \ ( F ` A ) ) ) = (/) -> ( F ` A ) =/= ( F ` suc A ) ) )
36 13 35 syl5 
 |-  ( A e. _om -> ( ( x \ ( F ` A ) ) =/= (/) -> ( F ` A ) =/= ( F ` suc A ) ) )
37 9 36 syldc 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= ( F ` suc A ) ) )