Metamath Proof Explorer

Theorem inf3lem6

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 inf3lem6 
|- ( ( x =/= (/) /\ x C_ U. x ) -> F : _om -1-1-> ~P 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 vex 
 |-  u e. _V
6 vex 
 |-  v e. _V
7 1 2 5 6 inf3lem5 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( ( u e. _om /\ v e. u ) -> ( F ` v ) C. ( F ` u ) ) )
8 dfpss2 
 |-  ( ( F ` v ) C. ( F ` u ) <-> ( ( F ` v ) C_ ( F ` u ) /\ -. ( F ` v ) = ( F ` u ) ) )
9 8 simprbi 
 |-  ( ( F ` v ) C. ( F ` u ) -> -. ( F ` v ) = ( F ` u ) )
10 7 9 syl6 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( ( u e. _om /\ v e. u ) -> -. ( F ` v ) = ( F ` u ) ) )
11 10 expdimp 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ u e. _om ) -> ( v e. u -> -. ( F ` v ) = ( F ` u ) ) )
12 11 adantrl 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ ( v e. _om /\ u e. _om ) ) -> ( v e. u -> -. ( F ` v ) = ( F ` u ) ) )
13 1 2 6 5 inf3lem5 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( ( v e. _om /\ u e. v ) -> ( F ` u ) C. ( F ` v ) ) )
14 dfpss2 
 |-  ( ( F ` u ) C. ( F ` v ) <-> ( ( F ` u ) C_ ( F ` v ) /\ -. ( F ` u ) = ( F ` v ) ) )
15 14 simprbi 
 |-  ( ( F ` u ) C. ( F ` v ) -> -. ( F ` u ) = ( F ` v ) )
16 eqcom 
 |-  ( ( F ` u ) = ( F ` v ) <-> ( F ` v ) = ( F ` u ) )
17 15 16 sylnib 
 |-  ( ( F ` u ) C. ( F ` v ) -> -. ( F ` v ) = ( F ` u ) )
18 13 17 syl6 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( ( v e. _om /\ u e. v ) -> -. ( F ` v ) = ( F ` u ) ) )
19 18 expdimp 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ v e. _om ) -> ( u e. v -> -. ( F ` v ) = ( F ` u ) ) )
20 19 adantrr 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ ( v e. _om /\ u e. _om ) ) -> ( u e. v -> -. ( F ` v ) = ( F ` u ) ) )
21 12 20 jaod 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ ( v e. _om /\ u e. _om ) ) -> ( ( v e. u \/ u e. v ) -> -. ( F ` v ) = ( F ` u ) ) )
22 21 con2d 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ ( v e. _om /\ u e. _om ) ) -> ( ( F ` v ) = ( F ` u ) -> -. ( v e. u \/ u e. v ) ) )
23 nnord 
 |-  ( v e. _om -> Ord v )
24 nnord 
 |-  ( u e. _om -> Ord u )
25 ordtri3 
 |-  ( ( Ord v /\ Ord u ) -> ( v = u <-> -. ( v e. u \/ u e. v ) ) )
26 23 24 25 syl2an 
 |-  ( ( v e. _om /\ u e. _om ) -> ( v = u <-> -. ( v e. u \/ u e. v ) ) )
27 26 adantl 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ ( v e. _om /\ u e. _om ) ) -> ( v = u <-> -. ( v e. u \/ u e. v ) ) )
28 22 27 sylibrd 
 |-  ( ( ( x =/= (/) /\ x C_ U. x ) /\ ( v e. _om /\ u e. _om ) ) -> ( ( F ` v ) = ( F ` u ) -> v = u ) )
29 28 ralrimivva 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> A. v e. _om A. u e. _om ( ( F ` v ) = ( F ` u ) -> v = u ) )
30 frfnom 
 |-  ( rec ( G , (/) ) |` _om ) Fn _om
31 fneq1 
 |-  ( F = ( rec ( G , (/) ) |` _om ) -> ( F Fn _om <-> ( rec ( G , (/) ) |` _om ) Fn _om ) )
32 30 31 mpbiri 
 |-  ( F = ( rec ( G , (/) ) |` _om ) -> F Fn _om )
33 fvelrnb 
 |-  ( F Fn _om -> ( u e. ran F <-> E. v e. _om ( F ` v ) = u ) )
34 1 2 6 4 inf3lemd 
 |-  ( v e. _om -> ( F ` v ) C_ x )
35 fvex 
 |-  ( F ` v ) e. _V
36 35 elpw 
 |-  ( ( F ` v ) e. ~P x <-> ( F ` v ) C_ x )
37 34 36 sylibr 
 |-  ( v e. _om -> ( F ` v ) e. ~P x )
38 eleq1 
 |-  ( ( F ` v ) = u -> ( ( F ` v ) e. ~P x <-> u e. ~P x ) )
39 37 38 syl5ibcom 
 |-  ( v e. _om -> ( ( F ` v ) = u -> u e. ~P x ) )
40 39 rexlimiv 
 |-  ( E. v e. _om ( F ` v ) = u -> u e. ~P x )
41 33 40 syl6bi 
 |-  ( F Fn _om -> ( u e. ran F -> u e. ~P x ) )
42 41 ssrdv 
 |-  ( F Fn _om -> ran F C_ ~P x )
43 42 ancli 
 |-  ( F Fn _om -> ( F Fn _om /\ ran F C_ ~P x ) )
44 2 32 43 mp2b 
 |-  ( F Fn _om /\ ran F C_ ~P x )
45 df-f 
 |-  ( F : _om --> ~P x <-> ( F Fn _om /\ ran F C_ ~P x ) )
46 44 45 mpbir 
 |-  F : _om --> ~P x
47 29 46 jctil 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( F : _om --> ~P x /\ A. v e. _om A. u e. _om ( ( F ` v ) = ( F ` u ) -> v = u ) ) )
48 dff13 
 |-  ( F : _om -1-1-> ~P x <-> ( F : _om --> ~P x /\ A. v e. _om A. u e. _om ( ( F ` v ) = ( F ` u ) -> v = u ) ) )
49 47 48 sylibr 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> F : _om -1-1-> ~P x )