Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex . (Contributed by NM, 29-Oct-1996) (Proof shortened by Mario Carneiro, 19-Jan-2013)
| 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 | inf3lem7 | |- ( ( x =/= (/) /\ x C_ U. x ) -> _om e. _V ) |
| 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 | inf3lem6 | |- ( ( x =/= (/) /\ x C_ U. x ) -> F : _om -1-1-> ~P x ) |
| 6 | vpwex | |- ~P x e. _V |
|
| 7 | f1dmex | |- ( ( F : _om -1-1-> ~P x /\ ~P x e. _V ) -> _om e. _V ) |
|
| 8 | 5 6 7 | sylancl | |- ( ( x =/= (/) /\ x C_ U. x ) -> _om e. _V ) |