MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunfictbso Unicode version

Theorem iunfictbso 8516
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.)
Assertion
Ref Expression
iunfictbso

Proof of Theorem iunfictbso
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omex 8081 . . . . 5
210dom 7667 . . . 4
3 breq1 4455 . . . 4
42, 3mpbiri 233 . . 3
54a1d 25 . 2
6 n0 3794 . . 3
7 ne0i 3790 . . . . . . . . . 10
8 unieq 4257 . . . . . . . . . . . 12
9 uni0 4276 . . . . . . . . . . . 12
108, 9syl6eq 2514 . . . . . . . . . . 11
1110necon3i 2697 . . . . . . . . . 10
127, 11syl 16 . . . . . . . . 9
1312adantl 466 . . . . . . . 8
14 simpl1 999 . . . . . . . . 9
15 reldom 7542 . . . . . . . . . 10
1615brrelexi 5045 . . . . . . . . 9
17 0sdomg 7666 . . . . . . . . 9
1814, 16, 173syl 20 . . . . . . . 8
1913, 18mpbird 232 . . . . . . 7
20 fodomr 7688 . . . . . . 7
2119, 14, 20syl2anc 661 . . . . . 6
22 omelon 8084 . . . . . . . . . . . 12
23 onenon 8351 . . . . . . . . . . . 12
2422, 23ax-mp 5 . . . . . . . . . . 11
25 xpnum 8353 . . . . . . . . . . 11
2624, 24, 25mp2an 672 . . . . . . . . . 10
27 simplrr 762 . . . . . . . . . . . . . . . . . . 19
28 fof 5800 . . . . . . . . . . . . . . . . . . 19
2927, 28syl 16 . . . . . . . . . . . . . . . . . 18
30 simprl 756 . . . . . . . . . . . . . . . . . 18
3129, 30ffvelrnd 6032 . . . . . . . . . . . . . . . . 17
3231adantr 465 . . . . . . . . . . . . . . . 16
33 elssuni 4279 . . . . . . . . . . . . . . . 16
3432, 33syl 16 . . . . . . . . . . . . . . 15
3531, 33syl 16 . . . . . . . . . . . . . . . . . . . . 21
36 simpll3 1037 . . . . . . . . . . . . . . . . . . . . 21
37 soss 4823 . . . . . . . . . . . . . . . . . . . . 21
3835, 36, 37sylc 60 . . . . . . . . . . . . . . . . . . . 20
39 simpll2 1036 . . . . . . . . . . . . . . . . . . . . 21
4039, 31sseldd 3504 . . . . . . . . . . . . . . . . . . . 20
41 finnisoeu 8515 . . . . . . . . . . . . . . . . . . . 20
4238, 40, 41syl2anc 661 . . . . . . . . . . . . . . . . . . 19
43 iotacl 5579 . . . . . . . . . . . . . . . . . . 19
4442, 43syl 16 . . . . . . . . . . . . . . . . . 18
45 iotaex 5573 . . . . . . . . . . . . . . . . . . 19
46 isoeq1 6215 . . . . . . . . . . . . . . . . . . 19 No typesetting for: |- ( 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 ) ) ) )
47 isoeq1 6215 . . . . . . . . . . . . . . . . . . . 20
4847cbvabv 2600 . . . . . . . . . . . . . . . . . . 19
4945, 46, 48elab2 3249 . . . . . . . . . . . . . . . . . 18 No typesetting for: |- ( ( 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 ) ) )
5044, 49sylib 196 . . . . . . . . . . . . . . . . 17 No typesetting for: |- ( ( ( ( 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 ) ) )
51 isof1o 6221 . . . . . . . . . . . . . . . . 17 No typesetting for: |- ( ( 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 ) )
52 f1of 5821 . . . . . . . . . . . . . . . . 17
5350, 51, 523syl 20 . . . . . . . . . . . . . . . 16
5453ffvelrnda 6031 . . . . . . . . . . . . . . 15
5534, 54sseldd 3504 . . . . . . . . . . . . . 14
56 simprl 756 . . . . . . . . . . . . . . 15
5756ad2antrr 725 . . . . . . . . . . . . . 14
5855, 57ifclda 3973 . . . . . . . . . . . . 13
5958ralrimivva 2878 . . . . . . . . . . . 12
60 eqid 2457 . . . . . . . . . . . . 13
6160fmpt2 6867 . . . . . . . . . . . 12
6259, 61sylib 196 . . . . . . . . . . 11
63 eluni 4252 . . . . . . . . . . . . 13
64 simplrr 762 . . . . . . . . . . . . . . . . 17
65 simprr 757 . . . . . . . . . . . . . . . . 17
66 foelrn 6050 . . . . . . . . . . . . . . . . 17
6764, 65, 66syl2anc 661 . . . . . . . . . . . . . . . 16
68 simprrl 765 . . . . . . . . . . . . . . . . . . . 20
69 ordom 6709 . . . . . . . . . . . . . . . . . . . . . 22
70 simpll2 1036 . . . . . . . . . . . . . . . . . . . . . . . 24
71 simplrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7271, 28syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
7372, 68ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . . . . . 24
7470, 73sseldd 3504 . . . . . . . . . . . . . . . . . . . . . . 23
75 ficardom 8363 . . . . . . . . . . . . . . . . . . . . . . 23
7674, 75syl 16 . . . . . . . . . . . . . . . . . . . . . 22
77 ordelss 4899 . . . . . . . . . . . . . . . . . . . . . 22
7869, 76, 77sylancr 663 . . . . . . . . . . . . . . . . . . . . 21
79 elssuni 4279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8073, 79syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81 simpll3 1037 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
82 soss 4823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8380, 81, 82sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
84 finnisoeu 8515 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8583, 74, 84syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
86 iotacl 5579 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8785, 86syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
88 iotaex 5573 . . . . . . . . . . . . . . . . . . . . . . . . . 26
89 isoeq1 6215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 No typesetting for: |- ( 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 ) ) ) )
90 isoeq1 6215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9190cbvabv 2600 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9288, 89, 91elab2 3249 . . . . . . . . . . . . . . . . . . . . . . . . 25 No typesetting for: |- ( ( 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 ) ) )
9387, 92sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24 No typesetting for: |- ( ( ( ( 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 ) ) )
94 isof1o 6221 . . . . . . . . . . . . . . . . . . . . . . . 24 No typesetting for: |- ( ( 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 ) )
9593, 94syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
96 f1ocnv 5833 . . . . . . . . . . . . . . . . . . . . . . 23
97 f1of 5821 . . . . . . . . . . . . . . . . . . . . . . 23
9895, 96, 973syl 20 . . . . . . . . . . . . . . . . . . . . . 22
99 simprll 763 . . . . . . . . . . . . . . . . . . . . . . 23
100 simprrr 766 . . . . . . . . . . . . . . . . . . . . . . 23
10199, 100eleqtrd 2547 . . . . . . . . . . . . . . . . . . . . . 22
10298, 101ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . . 21
10378, 102sseldd 3504 . . . . . . . . . . . . . . . . . . . 20
104 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
105104fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . 25
106105eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . . . 24
107 isoeq4 6218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
108105, 107syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
109 isoeq5 6219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110104, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
111108, 110bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . . . 26
112111iotabidv 5577 . . . . . . . . . . . . . . . . . . . . . . . . 25
113112fveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . 24
114106, 113ifbieq1d 3964 . . . . . . . . . . . . . . . . . . . . . . 23
115 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . 24
116 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . 24
117115, 116ifbieq1d 3964 . . . . . . . . . . . . . . . . . . . . . . 23
118 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . 24
119 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . 24
120118, 119ifex 4010 . . . . . . . . . . . . . . . . . . . . . . 23
121114, 117, 60, 120ovmpt2 6438 . . . . . . . . . . . . . . . . . . . . . 22
12268, 103, 121syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
123102iftrued 3949 . . . . . . . . . . . . . . . . . . . . 21
124 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . . . . . . 22
12595, 101, 124syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
126122, 123, 1253eqtrrd 2503 . . . . . . . . . . . . . . . . . . . 20