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 )