Metamath Proof Explorer

Theorem axcc2lem

Description: Lemma for axcc2 . (Contributed by Mario Carneiro, 8-Feb-2013)

Ref Expression
Hypotheses axcc2lem.1 
|- K = ( n e. _om |-> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) )
axcc2lem.2 
|- A = ( n e. _om |-> ( { n } X. ( K ` n ) ) )
axcc2lem.3 
|- G = ( n e. _om |-> ( 2nd ` ( f ` ( A ` n ) ) ) )
Assertion axcc2lem 
|- E. g ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) )

Proof

Step Hyp Ref Expression
1 axcc2lem.1 
 |-  K = ( n e. _om |-> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) )
2 axcc2lem.2 
 |-  A = ( n e. _om |-> ( { n } X. ( K ` n ) ) )
3 axcc2lem.3 
 |-  G = ( n e. _om |-> ( 2nd ` ( f ` ( A ` n ) ) ) )
4 fvex 
 |-  ( 2nd ` ( f ` ( A ` n ) ) ) e. _V
5 4 3 fnmpti 
 |-  G Fn _om
6 snex 
 |-  { n } e. _V
7 fvex 
 |-  ( K ` n ) e. _V
8 6 7 xpex 
 |-  ( { n } X. ( K ` n ) ) e. _V
9 2 fvmpt2 
 |-  ( ( n e. _om /\ ( { n } X. ( K ` n ) ) e. _V ) -> ( A ` n ) = ( { n } X. ( K ` n ) ) )
10 8 9 mpan2 
 |-  ( n e. _om -> ( A ` n ) = ( { n } X. ( K ` n ) ) )
11 vex 
 |-  n e. _V
12 11 snnz 
 |-  { n } =/= (/)
13 0ex 
 |-  (/) e. _V
14 13 snnz 
 |-  { (/) } =/= (/)
15 iftrue 
 |-  ( ( F ` n ) = (/) -> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) = { (/) } )
16 15 neeq1d 
 |-  ( ( F ` n ) = (/) -> ( if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) =/= (/) <-> { (/) } =/= (/) ) )
17 14 16 mpbiri 
 |-  ( ( F ` n ) = (/) -> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) =/= (/) )
18 iffalse 
 |-  ( -. ( F ` n ) = (/) -> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) = ( F ` n ) )
19 neqne 
 |-  ( -. ( F ` n ) = (/) -> ( F ` n ) =/= (/) )
20 18 19 eqnetrd 
 |-  ( -. ( F ` n ) = (/) -> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) =/= (/) )
21 17 20 pm2.61i 
 |-  if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) =/= (/)
22 p0ex 
 |-  { (/) } e. _V
23 fvex 
 |-  ( F ` n ) e. _V
24 22 23 ifex 
 |-  if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) e. _V
25 1 fvmpt2 
 |-  ( ( n e. _om /\ if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) e. _V ) -> ( K ` n ) = if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) )
26 24 25 mpan2 
 |-  ( n e. _om -> ( K ` n ) = if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) )
27 26 neeq1d 
 |-  ( n e. _om -> ( ( K ` n ) =/= (/) <-> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) =/= (/) ) )
28 21 27 mpbiri 
 |-  ( n e. _om -> ( K ` n ) =/= (/) )
29 xpnz 
 |-  ( ( { n } =/= (/) /\ ( K ` n ) =/= (/) ) <-> ( { n } X. ( K ` n ) ) =/= (/) )
30 29 biimpi 
 |-  ( ( { n } =/= (/) /\ ( K ` n ) =/= (/) ) -> ( { n } X. ( K ` n ) ) =/= (/) )
31 12 28 30 sylancr 
 |-  ( n e. _om -> ( { n } X. ( K ` n ) ) =/= (/) )
32 10 31 eqnetrd 
 |-  ( n e. _om -> ( A ` n ) =/= (/) )
33 8 2 fnmpti 
 |-  A Fn _om
34 fnfvelrn 
 |-  ( ( A Fn _om /\ n e. _om ) -> ( A ` n ) e. ran A )
35 33 34 mpan 
 |-  ( n e. _om -> ( A ` n ) e. ran A )
36 neeq1 
 |-  ( z = ( A ` n ) -> ( z =/= (/) <-> ( A ` n ) =/= (/) ) )
37 fveq2 
 |-  ( z = ( A ` n ) -> ( f ` z ) = ( f ` ( A ` n ) ) )
38 id 
 |-  ( z = ( A ` n ) -> z = ( A ` n ) )
39 37 38 eleq12d 
 |-  ( z = ( A ` n ) -> ( ( f ` z ) e. z <-> ( f ` ( A ` n ) ) e. ( A ` n ) ) )
40 36 39 imbi12d 
 |-  ( z = ( A ` n ) -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( ( A ` n ) =/= (/) -> ( f ` ( A ` n ) ) e. ( A ` n ) ) ) )
41 40 rspccv 
 |-  ( A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( A ` n ) e. ran A -> ( ( A ` n ) =/= (/) -> ( f ` ( A ` n ) ) e. ( A ` n ) ) ) )
42 35 41 syl5 
 |-  ( A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) -> ( n e. _om -> ( ( A ` n ) =/= (/) -> ( f ` ( A ` n ) ) e. ( A ` n ) ) ) )
43 32 42 mpdi 
 |-  ( A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) -> ( n e. _om -> ( f ` ( A ` n ) ) e. ( A ` n ) ) )
44 43 impcom 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( f ` ( A ` n ) ) e. ( A ` n ) )
45 10 eleq2d 
 |-  ( n e. _om -> ( ( f ` ( A ` n ) ) e. ( A ` n ) <-> ( f ` ( A ` n ) ) e. ( { n } X. ( K ` n ) ) ) )
46 45 adantr 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( f ` ( A ` n ) ) e. ( A ` n ) <-> ( f ` ( A ` n ) ) e. ( { n } X. ( K ` n ) ) ) )
47 44 46 mpbid 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( f ` ( A ` n ) ) e. ( { n } X. ( K ` n ) ) )
48 xp2nd 
 |-  ( ( f ` ( A ` n ) ) e. ( { n } X. ( K ` n ) ) -> ( 2nd ` ( f ` ( A ` n ) ) ) e. ( K ` n ) )
49 47 48 syl 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( 2nd ` ( f ` ( A ` n ) ) ) e. ( K ` n ) )
50 49 3adant3 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> ( 2nd ` ( f ` ( A ` n ) ) ) e. ( K ` n ) )
51 3 fvmpt2 
 |-  ( ( n e. _om /\ ( 2nd ` ( f ` ( A ` n ) ) ) e. _V ) -> ( G ` n ) = ( 2nd ` ( f ` ( A ` n ) ) ) )
52 4 51 mpan2 
 |-  ( n e. _om -> ( G ` n ) = ( 2nd ` ( f ` ( A ` n ) ) ) )
53 52 3ad2ant1 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> ( G ` n ) = ( 2nd ` ( f ` ( A ` n ) ) ) )
54 53 eqcomd 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> ( 2nd ` ( f ` ( A ` n ) ) ) = ( G ` n ) )
55 26 3ad2ant1 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> ( K ` n ) = if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) )
56 ifnefalse 
 |-  ( ( F ` n ) =/= (/) -> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) = ( F ` n ) )
57 56 3ad2ant3 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) = ( F ` n ) )
58 55 57 eqtrd 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> ( K ` n ) = ( F ` n ) )
59 50 54 58 3eltr3d 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) /\ ( F ` n ) =/= (/) ) -> ( G ` n ) e. ( F ` n ) )
60 59 3expia 
 |-  ( ( n e. _om /\ A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) )
61 60 expcom 
 |-  ( A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) -> ( n e. _om -> ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) ) )
62 61 ralrimiv 
 |-  ( A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) -> A. n e. _om ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) )
63 omex 
 |-  _om e. _V
64 fnex 
 |-  ( ( G Fn _om /\ _om e. _V ) -> G e. _V )
65 5 63 64 mp2an 
 |-  G e. _V
66 fneq1 
 |-  ( g = G -> ( g Fn _om <-> G Fn _om ) )
67 fveq1 
 |-  ( g = G -> ( g ` n ) = ( G ` n ) )
68 67 eleq1d 
 |-  ( g = G -> ( ( g ` n ) e. ( F ` n ) <-> ( G ` n ) e. ( F ` n ) ) )
69 68 imbi2d 
 |-  ( g = G -> ( ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) <-> ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) ) )
70 69 ralbidv 
 |-  ( g = G -> ( A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) <-> A. n e. _om ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) ) )
71 66 70 anbi12d 
 |-  ( g = G -> ( ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) ) <-> ( G Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) ) ) )
72 65 71 spcev 
 |-  ( ( G Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( G ` n ) e. ( F ` n ) ) ) -> E. g ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) ) )
73 5 62 72 sylancr 
 |-  ( A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) -> E. g ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) ) )
74 8 a1i 
 |-  ( ( _om e. _V /\ n e. _om ) -> ( { n } X. ( K ` n ) ) e. _V )
75 74 2 fmptd 
 |-  ( _om e. _V -> A : _om --> _V )
76 63 75 ax-mp 
 |-  A : _om --> _V
77 sneq 
 |-  ( n = k -> { n } = { k } )
78 fveq2 
 |-  ( n = k -> ( K ` n ) = ( K ` k ) )
79 77 78 xpeq12d 
 |-  ( n = k -> ( { n } X. ( K ` n ) ) = ( { k } X. ( K ` k ) ) )
80 79 2 8 fvmpt3i 
 |-  ( k e. _om -> ( A ` k ) = ( { k } X. ( K ` k ) ) )
81 80 adantl 
 |-  ( ( n e. _om /\ k e. _om ) -> ( A ` k ) = ( { k } X. ( K ` k ) ) )
82 81 eqeq2d 
 |-  ( ( n e. _om /\ k e. _om ) -> ( ( A ` n ) = ( A ` k ) <-> ( A ` n ) = ( { k } X. ( K ` k ) ) ) )
83 10 adantr 
 |-  ( ( n e. _om /\ k e. _om ) -> ( A ` n ) = ( { n } X. ( K ` n ) ) )
84 83 eqeq1d 
 |-  ( ( n e. _om /\ k e. _om ) -> ( ( A ` n ) = ( { k } X. ( K ` k ) ) <-> ( { n } X. ( K ` n ) ) = ( { k } X. ( K ` k ) ) ) )
85 xp11 
 |-  ( ( { n } =/= (/) /\ ( K ` n ) =/= (/) ) -> ( ( { n } X. ( K ` n ) ) = ( { k } X. ( K ` k ) ) <-> ( { n } = { k } /\ ( K ` n ) = ( K ` k ) ) ) )
86 12 28 85 sylancr 
 |-  ( n e. _om -> ( ( { n } X. ( K ` n ) ) = ( { k } X. ( K ` k ) ) <-> ( { n } = { k } /\ ( K ` n ) = ( K ` k ) ) ) )
87 11 sneqr 
 |-  ( { n } = { k } -> n = k )
88 87 adantr 
 |-  ( ( { n } = { k } /\ ( K ` n ) = ( K ` k ) ) -> n = k )
89 86 88 syl6bi 
 |-  ( n e. _om -> ( ( { n } X. ( K ` n ) ) = ( { k } X. ( K ` k ) ) -> n = k ) )
90 89 adantr 
 |-  ( ( n e. _om /\ k e. _om ) -> ( ( { n } X. ( K ` n ) ) = ( { k } X. ( K ` k ) ) -> n = k ) )
91 84 90 sylbid 
 |-  ( ( n e. _om /\ k e. _om ) -> ( ( A ` n ) = ( { k } X. ( K ` k ) ) -> n = k ) )
92 82 91 sylbid 
 |-  ( ( n e. _om /\ k e. _om ) -> ( ( A ` n ) = ( A ` k ) -> n = k ) )
93 92 rgen2 
 |-  A. n e. _om A. k e. _om ( ( A ` n ) = ( A ` k ) -> n = k )
94 dff13 
 |-  ( A : _om -1-1-> _V <-> ( A : _om --> _V /\ A. n e. _om A. k e. _om ( ( A ` n ) = ( A ` k ) -> n = k ) ) )
95 76 93 94 mpbir2an 
 |-  A : _om -1-1-> _V
96 f1f1orn 
 |-  ( A : _om -1-1-> _V -> A : _om -1-1-onto-> ran A )
97 63 f1oen 
 |-  ( A : _om -1-1-onto-> ran A -> _om ~~ ran A )
98 ensym 
 |-  ( _om ~~ ran A -> ran A ~~ _om )
99 96 97 98 3syl 
 |-  ( A : _om -1-1-> _V -> ran A ~~ _om )
100 2 rneqi 
 |-  ran A = ran ( n e. _om |-> ( { n } X. ( K ` n ) ) )
101 dmmptg 
 |-  ( A. n e. _om ( { n } X. ( K ` n ) ) e. _V -> dom ( n e. _om |-> ( { n } X. ( K ` n ) ) ) = _om )
102 8 a1i 
 |-  ( n e. _om -> ( { n } X. ( K ` n ) ) e. _V )
103 101 102 mprg 
 |-  dom ( n e. _om |-> ( { n } X. ( K ` n ) ) ) = _om
104 103 63 eqeltri 
 |-  dom ( n e. _om |-> ( { n } X. ( K ` n ) ) ) e. _V
105 funmpt 
 |-  Fun ( n e. _om |-> ( { n } X. ( K ` n ) ) )
106 funrnex 
 |-  ( dom ( n e. _om |-> ( { n } X. ( K ` n ) ) ) e. _V -> ( Fun ( n e. _om |-> ( { n } X. ( K ` n ) ) ) -> ran ( n e. _om |-> ( { n } X. ( K ` n ) ) ) e. _V ) )
107 104 105 106 mp2 
 |-  ran ( n e. _om |-> ( { n } X. ( K ` n ) ) ) e. _V
108 100 107 eqeltri 
 |-  ran A e. _V
109 breq1 
 |-  ( a = ran A -> ( a ~~ _om <-> ran A ~~ _om ) )
110 raleq 
 |-  ( a = ran A -> ( A. z e. a ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) )
111 110 exbidv 
 |-  ( a = ran A -> ( E. f A. z e. a ( z =/= (/) -> ( f ` z ) e. z ) <-> E. f A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) )
112 109 111 imbi12d 
 |-  ( a = ran A -> ( ( a ~~ _om -> E. f A. z e. a ( z =/= (/) -> ( f ` z ) e. z ) ) <-> ( ran A ~~ _om -> E. f A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) ) ) )
113 ax-cc 
 |-  ( a ~~ _om -> E. f A. z e. a ( z =/= (/) -> ( f ` z ) e. z ) )
114 108 112 113 vtocl 
 |-  ( ran A ~~ _om -> E. f A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z ) )
115 95 99 114 mp2b 
 |-  E. f A. z e. ran A ( z =/= (/) -> ( f ` z ) e. z )
116 73 115 exlimiiv 
 |-  E. g ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) )