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 ) ) )