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