Metamath Proof Explorer

Theorem iunfictbso

Description: Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion iunfictbso 
|- ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) -> U. A ~<_ _om )

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 1 0dom 
 |-  (/) ~<_ _om
3 breq1 
 |-  ( U. A = (/) -> ( U. A ~<_ _om <-> (/) ~<_ _om ) )
4 2 3 mpbiri 
 |-  ( U. A = (/) -> U. A ~<_ _om )
5 4 a1d 
 |-  ( U. A = (/) -> ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) -> U. A ~<_ _om ) )
6 n0 
 |-  ( U. A =/= (/) <-> E. a a e. U. A )
7 ne0i 
 |-  ( a e. U. A -> U. A =/= (/) )
8 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
9 uni0 
 |-  U. (/) = (/)
10 8 9 eqtrdi 
 |-  ( A = (/) -> U. A = (/) )
11 10 necon3i 
 |-  ( U. A =/= (/) -> A =/= (/) )
12 7 11 syl 
 |-  ( a e. U. A -> A =/= (/) )
13 12 adantl 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> A =/= (/) )
14 simpl1 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> A ~<_ _om )
15 ctex 
 |-  ( A ~<_ _om -> A e. _V )
16 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
17 14 15 16 3syl 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> ( (/) ~< A <-> A =/= (/) ) )
18 13 17 mpbird 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> (/) ~< A )
19 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ _om ) -> E. b b : _om -onto-> A )
20 18 14 19 syl2anc 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> E. b b : _om -onto-> A )
21 omelon 
 |-  _om e. On
22 onenon 
 |-  ( _om e. On -> _om e. dom card )
23 21 22 ax-mp 
 |-  _om e. dom card
24 xpnum 
 |-  ( ( _om e. dom card /\ _om e. dom card ) -> ( _om X. _om ) e. dom card )
25 23 23 24 mp2an 
 |-  ( _om X. _om ) e. dom card
26 simplrr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> b : _om -onto-> A )
27 fof 
 |-  ( b : _om -onto-> A -> b : _om --> A )
28 26 27 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> b : _om --> A )
29 simprl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> f e. _om )
30 28 29 ffvelrnd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> ( b ` f ) e. A )
31 30 adantr 
 |-  ( ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) /\ g e. ( card ` ( b ` f ) ) ) -> ( b ` f ) e. A )
32 elssuni 
 |-  ( ( b ` f ) e. A -> ( b ` f ) C_ U. A )
33 31 32 syl 
 |-  ( ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) /\ g e. ( card ` ( b ` f ) ) ) -> ( b ` f ) C_ U. A )
34 30 32 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> ( b ` f ) C_ U. A )
35 simpll3 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> B Or U. A )
36 soss 
 |-  ( ( b ` f ) C_ U. A -> ( B Or U. A -> B Or ( b ` f ) ) )
37 34 35 36 sylc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> B Or ( b ` f ) )
38 simpll2 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> A C_ Fin )
39 38 30 sseldd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> ( b ` f ) e. Fin )
40 finnisoeu 
 |-  ( ( B Or ( b ` f ) /\ ( b ` f ) e. Fin ) -> E! h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) )
41 37 39 40 syl2anc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> E! h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) )
42 iotacl 
 |-  ( E! h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) e. { h | h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) } )
43 41 42 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) e. { h | h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) } )
44 iotaex 
 |-  ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) e. _V
45 isoeq1 
 |-  ( a = ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) -> ( a Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) <-> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) )
46 isoeq1 
 |-  ( h = a -> ( h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) <-> a Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) )
47 46 cbvabv 
 |-  { h | h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) } = { a | a Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) }
48 44 45 47 elab2 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) e. { h | h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) } <-> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) )
49 43 48 sylib 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) )
50 isof1o 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) : ( card ` ( b ` f ) ) -1-1-onto-> ( b ` f ) )
51 f1of 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) : ( card ` ( b ` f ) ) -1-1-onto-> ( b ` f ) -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) : ( card ` ( b ` f ) ) --> ( b ` f ) )
52 49 50 51 3syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) : ( card ` ( b ` f ) ) --> ( b ` f ) )
53 52 ffvelrnda 
 |-  ( ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) /\ g e. ( card ` ( b ` f ) ) ) -> ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) e. ( b ` f ) )
54 33 53 sseldd 
 |-  ( ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) /\ g e. ( card ` ( b ` f ) ) ) -> ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) e. U. A )
55 simprl 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> a e. U. A )
56 55 ad2antrr 
 |-  ( ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) /\ -. g e. ( card ` ( b ` f ) ) ) -> a e. U. A )
57 54 56 ifclda 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( f e. _om /\ g e. _om ) ) -> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) e. U. A )
58 57 ralrimivva 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> A. f e. _om A. g e. _om if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) e. U. A )
59 eqid 
 |-  ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) = ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) )
60 59 fmpo 
 |-  ( A. f e. _om A. g e. _om if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) e. U. A <-> ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) : ( _om X. _om ) --> U. A )
61 58 60 sylib 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) : ( _om X. _om ) --> U. A )
62 eluni 
 |-  ( c e. U. A <-> E. i ( c e. i /\ i e. A ) )
63 simplrr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> b : _om -onto-> A )
64 simprr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> i e. A )
65 foelrn 
 |-  ( ( b : _om -onto-> A /\ i e. A ) -> E. j e. _om i = ( b ` j ) )
66 63 64 65 syl2anc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> E. j e. _om i = ( b ` j ) )
67 simprrl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> j e. _om )
68 ordom 
 |-  Ord _om
69 simpll2 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> A C_ Fin )
70 simplrr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> b : _om -onto-> A )
71 70 27 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> b : _om --> A )
72 71 67 ffvelrnd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( b ` j ) e. A )
73 69 72 sseldd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( b ` j ) e. Fin )
74 ficardom 
 |-  ( ( b ` j ) e. Fin -> ( card ` ( b ` j ) ) e. _om )
75 73 74 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( card ` ( b ` j ) ) e. _om )
76 ordelss 
 |-  ( ( Ord _om /\ ( card ` ( b ` j ) ) e. _om ) -> ( card ` ( b ` j ) ) C_ _om )
77 68 75 76 sylancr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( card ` ( b ` j ) ) C_ _om )
78 elssuni 
 |-  ( ( b ` j ) e. A -> ( b ` j ) C_ U. A )
79 72 78 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( b ` j ) C_ U. A )
80 simpll3 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> B Or U. A )
81 soss 
 |-  ( ( b ` j ) C_ U. A -> ( B Or U. A -> B Or ( b ` j ) ) )
82 79 80 81 sylc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> B Or ( b ` j ) )
83 finnisoeu 
 |-  ( ( B Or ( b ` j ) /\ ( b ` j ) e. Fin ) -> E! h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) )
84 82 73 83 syl2anc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> E! h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) )
85 iotacl 
 |-  ( E! h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) e. { h | h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) } )
86 84 85 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) e. { h | h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) } )
87 iotaex 
 |-  ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) e. _V
88 isoeq1 
 |-  ( a = ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) -> ( a Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) <-> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) )
89 isoeq1 
 |-  ( h = a -> ( h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) <-> a Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) )
90 89 cbvabv 
 |-  { h | h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) } = { a | a Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) }
91 87 88 90 elab2 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) e. { h | h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) } <-> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) )
92 86 91 sylib 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) )
93 isof1o 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( card ` ( b ` j ) ) -1-1-onto-> ( b ` j ) )
94 92 93 syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( card ` ( b ` j ) ) -1-1-onto-> ( b ` j ) )
95 f1ocnv 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( card ` ( b ` j ) ) -1-1-onto-> ( b ` j ) -> `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( b ` j ) -1-1-onto-> ( card ` ( b ` j ) ) )
96 f1of 
 |-  ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( b ` j ) -1-1-onto-> ( card ` ( b ` j ) ) -> `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( b ` j ) --> ( card ` ( b ` j ) ) )
97 94 95 96 3syl 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( b ` j ) --> ( card ` ( b ` j ) ) )
98 simprll 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> c e. i )
99 simprrr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> i = ( b ` j ) )
100 98 99 eleqtrd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> c e. ( b ` j ) )
101 97 100 ffvelrnd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) )
102 77 101 sseldd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. _om )
103 2fveq3 
 |-  ( f = j -> ( card ` ( b ` f ) ) = ( card ` ( b ` j ) ) )
104 103 eleq2d 
 |-  ( f = j -> ( g e. ( card ` ( b ` f ) ) <-> g e. ( card ` ( b ` j ) ) ) )
105 isoeq4 
 |-  ( ( card ` ( b ` f ) ) = ( card ` ( b ` j ) ) -> ( h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) <-> h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` f ) ) ) )
106 103 105 syl 
 |-  ( f = j -> ( h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) <-> h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` f ) ) ) )
107 fveq2 
 |-  ( f = j -> ( b ` f ) = ( b ` j ) )
108 isoeq5 
 |-  ( ( b ` f ) = ( b ` j ) -> ( h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` f ) ) <-> h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) )
109 107 108 syl 
 |-  ( f = j -> ( h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` f ) ) <-> h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) )
110 106 109 bitrd 
 |-  ( f = j -> ( h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) <-> h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) )
111 110 iotabidv 
 |-  ( f = j -> ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) = ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) )
112 111 fveq1d 
 |-  ( f = j -> ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) = ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` g ) )
113 104 112 ifbieq1d 
 |-  ( f = j -> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) = if ( g e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` g ) , a ) )
114 eleq1 
 |-  ( g = ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) -> ( g e. ( card ` ( b ` j ) ) <-> ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) ) )
115 fveq2 
 |-  ( g = ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) -> ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` g ) = ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) )
116 114 115 ifbieq1d 
 |-  ( g = ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) -> if ( g e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` g ) , a ) = if ( ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) , a ) )
117 fvex 
 |-  ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) e. _V
118 vex 
 |-  a e. _V
119 117 118 ifex 
 |-  if ( ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) , a ) e. _V
120 113 116 59 119 ovmpo 
 |-  ( ( j e. _om /\ ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. _om ) -> ( j ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) = if ( ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) , a ) )
121 67 102 120 syl2anc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( j ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) = if ( ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) , a ) )
122 101 iftrued 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> if ( ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. ( card ` ( b ` j ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) , a ) = ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) )
123 f1ocnvfv2 
 |-  ( ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) : ( card ` ( b ` j ) ) -1-1-onto-> ( b ` j ) /\ c e. ( b ` j ) ) -> ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) = c )
124 94 100 123 syl2anc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> ( ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) = c )
125 121 122 124 3eqtrrd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> c = ( j ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) )
126 rspceov 
 |-  ( ( j e. _om /\ ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) e. _om /\ c = ( j ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) ( `' ( iota h h Isom _E , B ( ( card ` ( b ` j ) ) , ( b ` j ) ) ) ` c ) ) ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) )
127 67 102 125 126 syl3anc 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( ( c e. i /\ i e. A ) /\ ( j e. _om /\ i = ( b ` j ) ) ) ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) )
128 127 expr 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> ( ( j e. _om /\ i = ( b ` j ) ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) )
129 128 expd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> ( j e. _om -> ( i = ( b ` j ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) ) )
130 129 rexlimdv 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> ( E. j e. _om i = ( b ` j ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) )
131 66 130 mpd 
 |-  ( ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) /\ ( c e. i /\ i e. A ) ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) )
132 131 ex 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> ( ( c e. i /\ i e. A ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) )
133 132 exlimdv 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> ( E. i ( c e. i /\ i e. A ) -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) )
134 62 133 syl5bi 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> ( c e. U. A -> E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) )
135 134 ralrimiv 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> A. c e. U. A E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) )
136 foov 
 |-  ( ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) : ( _om X. _om ) -onto-> U. A <-> ( ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) : ( _om X. _om ) --> U. A /\ A. c e. U. A E. d e. _om E. e e. _om c = ( d ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) e ) ) )
137 61 135 136 sylanbrc 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) : ( _om X. _om ) -onto-> U. A )
138 fodomnum 
 |-  ( ( _om X. _om ) e. dom card -> ( ( f e. _om , g e. _om |-> if ( g e. ( card ` ( b ` f ) ) , ( ( iota h h Isom _E , B ( ( card ` ( b ` f ) ) , ( b ` f ) ) ) ` g ) , a ) ) : ( _om X. _om ) -onto-> U. A -> U. A ~<_ ( _om X. _om ) ) )
139 25 137 138 mpsyl 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> U. A ~<_ ( _om X. _om ) )
140 xpomen 
 |-  ( _om X. _om ) ~~ _om
141 domentr 
 |-  ( ( U. A ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> U. A ~<_ _om )
142 139 140 141 sylancl 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ ( a e. U. A /\ b : _om -onto-> A ) ) -> U. A ~<_ _om )
143 142 expr 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> ( b : _om -onto-> A -> U. A ~<_ _om ) )
144 143 exlimdv 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> ( E. b b : _om -onto-> A -> U. A ~<_ _om ) )
145 20 144 mpd 
 |-  ( ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) /\ a e. U. A ) -> U. A ~<_ _om )
146 145 expcom 
 |-  ( a e. U. A -> ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) -> U. A ~<_ _om ) )
147 146 exlimiv 
 |-  ( E. a a e. U. A -> ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) -> U. A ~<_ _om ) )
148 6 147 sylbi 
 |-  ( U. A =/= (/) -> ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) -> U. A ~<_ _om ) )
149 5 148 pm2.61ine 
 |-  ( ( A ~<_ _om /\ A C_ Fin /\ B Or U. A ) -> U. A ~<_ _om )