Step |
Hyp |
Ref |
Expression |
1 |
|
infxpidm2 |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A ) |
2 |
|
infn0 |
|- ( _om ~<_ A -> A =/= (/) ) |
3 |
2
|
adantl |
|- ( ( A e. dom card /\ _om ~<_ A ) -> A =/= (/) ) |
4 |
|
fseqen |
|- ( ( ( A X. A ) ~~ A /\ A =/= (/) ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) ) |
5 |
1 3 4
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) ) |
6 |
|
xpdom1g |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( _om X. A ) ~<_ ( A X. A ) ) |
7 |
|
domentr |
|- ( ( ( _om X. A ) ~<_ ( A X. A ) /\ ( A X. A ) ~~ A ) -> ( _om X. A ) ~<_ A ) |
8 |
6 1 7
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( _om X. A ) ~<_ A ) |
9 |
|
endomtr |
|- ( ( U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) /\ ( _om X. A ) ~<_ A ) -> U_ n e. _om ( A ^m n ) ~<_ A ) |
10 |
5 8 9
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> U_ n e. _om ( A ^m n ) ~<_ A ) |
11 |
|
numdom |
|- ( ( A e. dom card /\ U_ n e. _om ( A ^m n ) ~<_ A ) -> U_ n e. _om ( A ^m n ) e. dom card ) |
12 |
10 11
|
syldan |
|- ( ( A e. dom card /\ _om ~<_ A ) -> U_ n e. _om ( A ^m n ) e. dom card ) |
13 |
|
eliun |
|- ( x e. U_ n e. _om ( A ^m n ) <-> E. n e. _om x e. ( A ^m n ) ) |
14 |
|
elmapi |
|- ( x e. ( A ^m n ) -> x : n --> A ) |
15 |
14
|
ad2antll |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> x : n --> A ) |
16 |
15
|
frnd |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x C_ A ) |
17 |
|
vex |
|- x e. _V |
18 |
17
|
rnex |
|- ran x e. _V |
19 |
18
|
elpw |
|- ( ran x e. ~P A <-> ran x C_ A ) |
20 |
16 19
|
sylibr |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x e. ~P A ) |
21 |
|
simprl |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> n e. _om ) |
22 |
|
ssid |
|- n C_ n |
23 |
|
ssnnfi |
|- ( ( n e. _om /\ n C_ n ) -> n e. Fin ) |
24 |
21 22 23
|
sylancl |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> n e. Fin ) |
25 |
|
ffn |
|- ( x : n --> A -> x Fn n ) |
26 |
|
dffn4 |
|- ( x Fn n <-> x : n -onto-> ran x ) |
27 |
25 26
|
sylib |
|- ( x : n --> A -> x : n -onto-> ran x ) |
28 |
15 27
|
syl |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> x : n -onto-> ran x ) |
29 |
|
fofi |
|- ( ( n e. Fin /\ x : n -onto-> ran x ) -> ran x e. Fin ) |
30 |
24 28 29
|
syl2anc |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x e. Fin ) |
31 |
20 30
|
elind |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x e. ( ~P A i^i Fin ) ) |
32 |
31
|
expr |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ n e. _om ) -> ( x e. ( A ^m n ) -> ran x e. ( ~P A i^i Fin ) ) ) |
33 |
32
|
rexlimdva |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( E. n e. _om x e. ( A ^m n ) -> ran x e. ( ~P A i^i Fin ) ) ) |
34 |
13 33
|
syl5bi |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) -> ran x e. ( ~P A i^i Fin ) ) ) |
35 |
34
|
imp |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ x e. U_ n e. _om ( A ^m n ) ) -> ran x e. ( ~P A i^i Fin ) ) |
36 |
35
|
fmpttd |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) --> ( ~P A i^i Fin ) ) |
37 |
36
|
ffnd |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) Fn U_ n e. _om ( A ^m n ) ) |
38 |
36
|
frnd |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) C_ ( ~P A i^i Fin ) ) |
39 |
|
simpr |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> y e. ( ~P A i^i Fin ) ) |
40 |
39
|
elin2d |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin ) |
41 |
|
isfi |
|- ( y e. Fin <-> E. m e. _om y ~~ m ) |
42 |
40 41
|
sylib |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> E. m e. _om y ~~ m ) |
43 |
|
ensym |
|- ( y ~~ m -> m ~~ y ) |
44 |
|
bren |
|- ( m ~~ y <-> E. x x : m -1-1-onto-> y ) |
45 |
43 44
|
sylib |
|- ( y ~~ m -> E. x x : m -1-1-onto-> y ) |
46 |
|
simprl |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> m e. _om ) |
47 |
|
f1of |
|- ( x : m -1-1-onto-> y -> x : m --> y ) |
48 |
47
|
ad2antll |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x : m --> y ) |
49 |
|
simplr |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y e. ( ~P A i^i Fin ) ) |
50 |
49
|
elin1d |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y e. ~P A ) |
51 |
50
|
elpwid |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y C_ A ) |
52 |
48 51
|
fssd |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x : m --> A ) |
53 |
|
simplll |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> A e. dom card ) |
54 |
|
vex |
|- m e. _V |
55 |
|
elmapg |
|- ( ( A e. dom card /\ m e. _V ) -> ( x e. ( A ^m m ) <-> x : m --> A ) ) |
56 |
53 54 55
|
sylancl |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> ( x e. ( A ^m m ) <-> x : m --> A ) ) |
57 |
52 56
|
mpbird |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x e. ( A ^m m ) ) |
58 |
|
oveq2 |
|- ( n = m -> ( A ^m n ) = ( A ^m m ) ) |
59 |
58
|
eleq2d |
|- ( n = m -> ( x e. ( A ^m n ) <-> x e. ( A ^m m ) ) ) |
60 |
59
|
rspcev |
|- ( ( m e. _om /\ x e. ( A ^m m ) ) -> E. n e. _om x e. ( A ^m n ) ) |
61 |
46 57 60
|
syl2anc |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> E. n e. _om x e. ( A ^m n ) ) |
62 |
61 13
|
sylibr |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x e. U_ n e. _om ( A ^m n ) ) |
63 |
|
f1ofo |
|- ( x : m -1-1-onto-> y -> x : m -onto-> y ) |
64 |
63
|
ad2antll |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x : m -onto-> y ) |
65 |
|
forn |
|- ( x : m -onto-> y -> ran x = y ) |
66 |
64 65
|
syl |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> ran x = y ) |
67 |
66
|
eqcomd |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y = ran x ) |
68 |
62 67
|
jca |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) |
69 |
68
|
expr |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ m e. _om ) -> ( x : m -1-1-onto-> y -> ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) ) |
70 |
69
|
eximdv |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ m e. _om ) -> ( E. x x : m -1-1-onto-> y -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) ) |
71 |
45 70
|
syl5 |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ m e. _om ) -> ( y ~~ m -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) ) |
72 |
71
|
rexlimdva |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> ( E. m e. _om y ~~ m -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) ) |
73 |
42 72
|
mpd |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) |
74 |
73
|
ex |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( y e. ( ~P A i^i Fin ) -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) ) |
75 |
|
eqid |
|- ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) = ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) |
76 |
75
|
elrnmpt |
|- ( y e. _V -> ( y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) <-> E. x e. U_ n e. _om ( A ^m n ) y = ran x ) ) |
77 |
76
|
elv |
|- ( y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) <-> E. x e. U_ n e. _om ( A ^m n ) y = ran x ) |
78 |
|
df-rex |
|- ( E. x e. U_ n e. _om ( A ^m n ) y = ran x <-> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) |
79 |
77 78
|
bitri |
|- ( y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) <-> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) |
80 |
74 79
|
syl6ibr |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( y e. ( ~P A i^i Fin ) -> y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) ) ) |
81 |
80
|
ssrdv |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) C_ ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) ) |
82 |
38 81
|
eqssd |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) = ( ~P A i^i Fin ) ) |
83 |
|
df-fo |
|- ( ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) -onto-> ( ~P A i^i Fin ) <-> ( ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) Fn U_ n e. _om ( A ^m n ) /\ ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) = ( ~P A i^i Fin ) ) ) |
84 |
37 82 83
|
sylanbrc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) -onto-> ( ~P A i^i Fin ) ) |
85 |
|
fodomnum |
|- ( U_ n e. _om ( A ^m n ) e. dom card -> ( ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) -onto-> ( ~P A i^i Fin ) -> ( ~P A i^i Fin ) ~<_ U_ n e. _om ( A ^m n ) ) ) |
86 |
12 84 85
|
sylc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~<_ U_ n e. _om ( A ^m n ) ) |
87 |
|
domtr |
|- ( ( ( ~P A i^i Fin ) ~<_ U_ n e. _om ( A ^m n ) /\ U_ n e. _om ( A ^m n ) ~<_ A ) -> ( ~P A i^i Fin ) ~<_ A ) |
88 |
86 10 87
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~<_ A ) |
89 |
|
pwexg |
|- ( A e. dom card -> ~P A e. _V ) |
90 |
89
|
adantr |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ~P A e. _V ) |
91 |
|
inex1g |
|- ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V ) |
92 |
90 91
|
syl |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) e. _V ) |
93 |
|
infpwfidom |
|- ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) ) |
94 |
92 93
|
syl |
|- ( ( A e. dom card /\ _om ~<_ A ) -> A ~<_ ( ~P A i^i Fin ) ) |
95 |
|
sbth |
|- ( ( ( ~P A i^i Fin ) ~<_ A /\ A ~<_ ( ~P A i^i Fin ) ) -> ( ~P A i^i Fin ) ~~ A ) |
96 |
88 94 95
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~~ A ) |