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 imbitrdi 
 |-  ( 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 biimtrrid 
 |-  ( f e. ( G ` ( F ` u ) ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) )
42 34 41 biimtrdi 
 |-  ( 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 ) )