Metamath Proof Explorer

Theorem dcomex

Description: The Axiom of Dependent Choice implies Infinity, the way we have stated it. Thus, we haveInf+AC impliesDC andDC impliesInf, but AC does not implyInf. (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Assertion dcomex 
|- _om e. _V

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 df-br 
 |-  ( ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) <-> <. ( f ` n ) , ( f ` suc n ) >. e. { <. 1o , 1o >. } )
3 elsni 
 |-  ( <. ( f ` n ) , ( f ` suc n ) >. e. { <. 1o , 1o >. } -> <. ( f ` n ) , ( f ` suc n ) >. = <. 1o , 1o >. )
4 fvex 
 |-  ( f ` n ) e. _V
5 fvex 
 |-  ( f ` suc n ) e. _V
6 4 5 opth1 
 |-  ( <. ( f ` n ) , ( f ` suc n ) >. = <. 1o , 1o >. -> ( f ` n ) = 1o )
7 3 6 syl 
 |-  ( <. ( f ` n ) , ( f ` suc n ) >. e. { <. 1o , 1o >. } -> ( f ` n ) = 1o )
8 2 7 sylbi 
 |-  ( ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) -> ( f ` n ) = 1o )
9 tz6.12i 
 |-  ( 1o =/= (/) -> ( ( f ` n ) = 1o -> n f 1o ) )
10 1 8 9 mpsyl 
 |-  ( ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) -> n f 1o )
11 vex 
 |-  n e. _V
12 1oex 
 |-  1o e. _V
13 11 12 breldm 
 |-  ( n f 1o -> n e. dom f )
14 10 13 syl 
 |-  ( ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) -> n e. dom f )
15 14 ralimi 
 |-  ( A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) -> A. n e. _om n e. dom f )
16 dfss3 
 |-  ( _om C_ dom f <-> A. n e. _om n e. dom f )
17 15 16 sylibr 
 |-  ( A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) -> _om C_ dom f )
18 vex 
 |-  f e. _V
19 18 dmex 
 |-  dom f e. _V
20 19 ssex 
 |-  ( _om C_ dom f -> _om e. _V )
21 17 20 syl 
 |-  ( A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) -> _om e. _V )
22 snex 
 |-  { <. 1o , 1o >. } e. _V
23 12 12 fvsn 
 |-  ( { <. 1o , 1o >. } ` 1o ) = 1o
24 12 12 funsn 
 |-  Fun { <. 1o , 1o >. }
25 12 snid 
 |-  1o e. { 1o }
26 12 dmsnop 
 |-  dom { <. 1o , 1o >. } = { 1o }
27 25 26 eleqtrri 
 |-  1o e. dom { <. 1o , 1o >. }
28 funbrfvb 
 |-  ( ( Fun { <. 1o , 1o >. } /\ 1o e. dom { <. 1o , 1o >. } ) -> ( ( { <. 1o , 1o >. } ` 1o ) = 1o <-> 1o { <. 1o , 1o >. } 1o ) )
29 24 27 28 mp2an 
 |-  ( ( { <. 1o , 1o >. } ` 1o ) = 1o <-> 1o { <. 1o , 1o >. } 1o )
30 23 29 mpbi 
 |-  1o { <. 1o , 1o >. } 1o
31 breq12 
 |-  ( ( s = 1o /\ t = 1o ) -> ( s { <. 1o , 1o >. } t <-> 1o { <. 1o , 1o >. } 1o ) )
32 12 12 31 spc2ev 
 |-  ( 1o { <. 1o , 1o >. } 1o -> E. s E. t s { <. 1o , 1o >. } t )
33 30 32 ax-mp 
 |-  E. s E. t s { <. 1o , 1o >. } t
34 breq 
 |-  ( x = { <. 1o , 1o >. } -> ( s x t <-> s { <. 1o , 1o >. } t ) )
35 34 2exbidv 
 |-  ( x = { <. 1o , 1o >. } -> ( E. s E. t s x t <-> E. s E. t s { <. 1o , 1o >. } t ) )
36 33 35 mpbiri 
 |-  ( x = { <. 1o , 1o >. } -> E. s E. t s x t )
37 ssid 
 |-  { 1o } C_ { 1o }
38 12 rnsnop 
 |-  ran { <. 1o , 1o >. } = { 1o }
39 37 38 26 3sstr4i 
 |-  ran { <. 1o , 1o >. } C_ dom { <. 1o , 1o >. }
40 rneq 
 |-  ( x = { <. 1o , 1o >. } -> ran x = ran { <. 1o , 1o >. } )
41 dmeq 
 |-  ( x = { <. 1o , 1o >. } -> dom x = dom { <. 1o , 1o >. } )
42 40 41 sseq12d 
 |-  ( x = { <. 1o , 1o >. } -> ( ran x C_ dom x <-> ran { <. 1o , 1o >. } C_ dom { <. 1o , 1o >. } ) )
43 39 42 mpbiri 
 |-  ( x = { <. 1o , 1o >. } -> ran x C_ dom x )
44 pm5.5 
 |-  ( ( E. s E. t s x t /\ ran x C_ dom x ) -> ( ( ( E. s E. t s x t /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) <-> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) )
45 36 43 44 syl2anc 
 |-  ( x = { <. 1o , 1o >. } -> ( ( ( E. s E. t s x t /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) <-> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) )
46 breq 
 |-  ( x = { <. 1o , 1o >. } -> ( ( f ` n ) x ( f ` suc n ) <-> ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) ) )
47 46 ralbidv 
 |-  ( x = { <. 1o , 1o >. } -> ( A. n e. _om ( f ` n ) x ( f ` suc n ) <-> A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) ) )
48 47 exbidv 
 |-  ( x = { <. 1o , 1o >. } -> ( E. f A. n e. _om ( f ` n ) x ( f ` suc n ) <-> E. f A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) ) )
49 45 48 bitrd 
 |-  ( x = { <. 1o , 1o >. } -> ( ( ( E. s E. t s x t /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) <-> E. f A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n ) ) )
50 ax-dc 
 |-  ( ( E. s E. t s x t /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) )
51 22 49 50 vtocl 
 |-  E. f A. n e. _om ( f ` n ) { <. 1o , 1o >. } ( f ` suc n )
52 21 51 exlimiiv 
 |-  _om e. _V