Metamath Proof Explorer


Theorem inf3lem2

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-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 inf3lem2
|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= 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 fveq2
 |-  ( v = (/) -> ( F ` v ) = ( F ` (/) ) )
6 5 neeq1d
 |-  ( v = (/) -> ( ( F ` v ) =/= x <-> ( F ` (/) ) =/= x ) )
7 6 imbi2d
 |-  ( v = (/) -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` (/) ) =/= x ) ) )
8 fveq2
 |-  ( v = u -> ( F ` v ) = ( F ` u ) )
9 8 neeq1d
 |-  ( v = u -> ( ( F ` v ) =/= x <-> ( F ` u ) =/= x ) )
10 9 imbi2d
 |-  ( v = u -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` u ) =/= x ) ) )
11 fveq2
 |-  ( v = suc u -> ( F ` v ) = ( F ` suc u ) )
12 11 neeq1d
 |-  ( v = suc u -> ( ( F ` v ) =/= x <-> ( F ` suc u ) =/= x ) )
13 12 imbi2d
 |-  ( v = suc u -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` suc u ) =/= x ) ) )
14 fveq2
 |-  ( v = A -> ( F ` v ) = ( F ` A ) )
15 14 neeq1d
 |-  ( v = A -> ( ( F ` v ) =/= x <-> ( F ` A ) =/= x ) )
16 15 imbi2d
 |-  ( v = A -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` A ) =/= x ) ) )
17 1 2 3 4 inf3lemb
 |-  ( F ` (/) ) = (/)
18 17 eqeq1i
 |-  ( ( F ` (/) ) = x <-> (/) = x )
19 eqcom
 |-  ( (/) = x <-> x = (/) )
20 18 19 sylbb
 |-  ( ( F ` (/) ) = x -> x = (/) )
21 20 necon3i
 |-  ( x =/= (/) -> ( F ` (/) ) =/= x )
22 21 adantr
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` (/) ) =/= x )
23 vex
 |-  u e. _V
24 1 2 23 4 inf3lemd
 |-  ( u e. _om -> ( F ` u ) C_ x )
25 df-pss
 |-  ( ( F ` u ) C. x <-> ( ( F ` u ) C_ x /\ ( F ` u ) =/= x ) )
26 pssnel
 |-  ( ( F ` u ) C. x -> E. v ( v e. x /\ -. v e. ( F ` u ) ) )
27 25 26 sylbir
 |-  ( ( ( F ` u ) C_ x /\ ( F ` u ) =/= x ) -> E. v ( v e. x /\ -. v e. ( F ` u ) ) )
28 ssel
 |-  ( x C_ U. x -> ( v e. x -> v e. U. x ) )
29 eluni
 |-  ( v e. U. x <-> E. f ( v e. f /\ f e. x ) )
30 28 29 syl6ib
 |-  ( x C_ U. x -> ( v e. x -> E. f ( v e. f /\ f e. x ) ) )
31 eleq2
 |-  ( ( F ` suc u ) = x -> ( f e. ( F ` suc u ) <-> f e. x ) )
32 31 biimparc
 |-  ( ( f e. x /\ ( F ` suc u ) = x ) -> f e. ( F ` suc u ) )
33 1 2 23 4 inf3lemc
 |-  ( u e. _om -> ( F ` suc u ) = ( G ` ( F ` u ) ) )
34 33 eleq2d
 |-  ( u e. _om -> ( f e. ( F ` suc u ) <-> f e. ( G ` ( F ` u ) ) ) )
35 elin
 |-  ( v e. ( f i^i x ) <-> ( v e. f /\ v e. x ) )
36 vex
 |-  f e. _V
37 fvex
 |-  ( F ` u ) e. _V
38 1 2 36 37 inf3lema
 |-  ( f e. ( G ` ( F ` u ) ) <-> ( f e. x /\ ( f i^i x ) C_ ( F ` u ) ) )
39 38 simprbi
 |-  ( f e. ( G ` ( F ` u ) ) -> ( f i^i x ) C_ ( F ` u ) )
40 39 sseld
 |-  ( f e. ( G ` ( F ` u ) ) -> ( v e. ( f i^i x ) -> v e. ( F ` u ) ) )
41 35 40 syl5bir
 |-  ( f e. ( G ` ( F ` u ) ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) )
42 34 41 syl6bi
 |-  ( u e. _om -> ( f e. ( F ` suc u ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) ) )
43 32 42 syl5
 |-  ( u e. _om -> ( ( f e. x /\ ( F ` suc u ) = x ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) ) )
44 43 com23
 |-  ( u e. _om -> ( ( v e. f /\ v e. x ) -> ( ( f e. x /\ ( F ` suc u ) = x ) -> v e. ( F ` u ) ) ) )
45 44 exp5c
 |-  ( u e. _om -> ( v e. f -> ( v e. x -> ( f e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) )
46 45 com34
 |-  ( u e. _om -> ( v e. f -> ( f e. x -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) )
47 46 impd
 |-  ( u e. _om -> ( ( v e. f /\ f e. x ) -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) )
48 47 exlimdv
 |-  ( u e. _om -> ( E. f ( v e. f /\ f e. x ) -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) )
49 30 48 sylan9r
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( v e. x -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) )
50 49 pm2.43d
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) )
51 id
 |-  ( ( ( F ` suc u ) = x -> v e. ( F ` u ) ) -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) )
52 51 necon3bd
 |-  ( ( ( F ` suc u ) = x -> v e. ( F ` u ) ) -> ( -. v e. ( F ` u ) -> ( F ` suc u ) =/= x ) )
53 50 52 syl6
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( v e. x -> ( -. v e. ( F ` u ) -> ( F ` suc u ) =/= x ) ) )
54 53 impd
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( ( v e. x /\ -. v e. ( F ` u ) ) -> ( F ` suc u ) =/= x ) )
55 54 exlimdv
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( E. v ( v e. x /\ -. v e. ( F ` u ) ) -> ( F ` suc u ) =/= x ) )
56 27 55 syl5
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( ( ( F ` u ) C_ x /\ ( F ` u ) =/= x ) -> ( F ` suc u ) =/= x ) )
57 24 56 sylani
 |-  ( ( u e. _om /\ x C_ U. x ) -> ( ( u e. _om /\ ( F ` u ) =/= x ) -> ( F ` suc u ) =/= x ) )
58 57 exp4b
 |-  ( u e. _om -> ( x C_ U. x -> ( u e. _om -> ( ( F ` u ) =/= x -> ( F ` suc u ) =/= x ) ) ) )
59 58 pm2.43a
 |-  ( u e. _om -> ( x C_ U. x -> ( ( F ` u ) =/= x -> ( F ` suc u ) =/= x ) ) )
60 59 adantld
 |-  ( u e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( ( F ` u ) =/= x -> ( F ` suc u ) =/= x ) ) )
61 60 a2d
 |-  ( u e. _om -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` u ) =/= x ) -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` suc u ) =/= x ) ) )
62 7 10 13 16 22 61 finds
 |-  ( A e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` A ) =/= x ) )
63 62 com12
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= x ) )