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

Theorem iundom2g 8415
 Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. depends on and should be thought of as . (Contributed by Mario Carneiro, 1-Sep-2015.)
Hypotheses
Ref Expression
iunfo.1
iundomg.2 AC
iundomg.3
Assertion
Ref Expression
iundom2g
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem iundom2g
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iundomg.2 . . 3 AC
2 iundomg.3 . . . . 5
3 brdomi 7119 . . . . . . . . 9
43adantl 453 . . . . . . . 8
5 f1f 5639 . . . . . . . . . . . 12
6 reldom 7115 . . . . . . . . . . . . . . 15
76brrelex2i 4919 . . . . . . . . . . . . . 14
86brrelexi 4918 . . . . . . . . . . . . . 14
9 elmapg 7031 . . . . . . . . . . . . . 14
107, 8, 9syl2anc 643 . . . . . . . . . . . . 13
1110adantl 453 . . . . . . . . . . . 12
125, 11syl5ibr 213 . . . . . . . . . . 11
13 ssiun2 4134 . . . . . . . . . . . . 13
1413adantr 452 . . . . . . . . . . . 12
1514sseld 3347 . . . . . . . . . . 11
1612, 15syld 42 . . . . . . . . . 10
1716ancrd 538 . . . . . . . . 9
1817eximdv 1632 . . . . . . . 8
194, 18mpd 15 . . . . . . 7
20 df-rex 2711 . . . . . . 7
2119, 20sylibr 204 . . . . . 6
2221ralimiaa 2780 . . . . 5
232, 22syl 16 . . . 4
24 nfv 1629 . . . . 5
25 nfiu1 4121 . . . . . 6
26 nfcv 2572 . . . . . . 7
27 nfcsb1v 3283 . . . . . . 7
28 nfcv 2572 . . . . . . 7
2926, 27, 28nff1 5637 . . . . . 6
3025, 29nfrex 2761 . . . . 5
31 csbeq1a 3259 . . . . . . 7
32 f1eq2 5635 . . . . . . 7
3331, 32syl 16 . . . . . 6
3433rexbidv 2726 . . . . 5
3524, 30, 34cbvral 2928 . . . 4
3623, 35sylib 189 . . 3
37 f1eq1 5634 . . . 4
3837acni3 7928 . . 3 AC
391, 36, 38syl2anc 643 . 2
40 nfv 1629 . . . . . 6
41 nfcv 2572 . . . . . . 7
4241, 27, 28nff1 5637 . . . . . 6
43 fveq2 5728 . . . . . . . 8
44 f1eq1 5634 . . . . . . . 8
4543, 44syl 16 . . . . . . 7
46 f1eq2 5635 . . . . . . . 8
4731, 46syl 16 . . . . . . 7
4845, 47bitrd 245 . . . . . 6
4940, 42, 48cbvral 2928 . . . . 5
50 df-ne 2601 . . . . . . . 8
51 acnrcl 7923 . . . . . . . . . 10 AC
521, 51syl 16 . . . . . . . . 9
53 r19.2z 3717 . . . . . . . . . . . 12
547rexlimivw 2826 . . . . . . . . . . . 12
5553, 54syl 16 . . . . . . . . . . 11
5655expcom 425 . . . . . . . . . 10
572, 56syl 16 . . . . . . . . 9
58 xpexg 4989 . . . . . . . . 9
5952, 57, 58ee12an 1372 . . . . . . . 8
6050, 59syl5bir 210 . . . . . . 7
61 xpeq1 4892 . . . . . . . 8
62 xp0r 4956 . . . . . . . . 9
63 0ex 4339 . . . . . . . . 9
6462, 63eqeltri 2506 . . . . . . . 8
6561, 64syl6eqel 2524 . . . . . . 7
6660, 65pm2.61d2 154 . . . . . 6
67 iunfo.1 . . . . . . . . . 10
6867eleq2i 2500 . . . . . . . . 9
69 eliun 4097 . . . . . . . . 9
7068, 69bitri 241 . . . . . . . 8
71 r19.29 2846 . . . . . . . . . 10
72 xp1st 6376 . . . . . . . . . . . . . . 15
7372ad2antll 710 . . . . . . . . . . . . . 14
74 elsni 3838 . . . . . . . . . . . . . 14
7573, 74syl 16 . . . . . . . . . . . . 13
76 simpl 444 . . . . . . . . . . . . 13
7775, 76eqeltrd 2510 . . . . . . . . . . . 12
7875fveq2d 5732 . . . . . . . . . . . . . 14
7978fveq1d 5730 . . . . . . . . . . . . 13
80 f1f 5639 . . . . . . . . . . . . . . 15
8180ad2antrl 709 . . . . . . . . . . . . . 14
82 xp2nd 6377 . . . . . . . . . . . . . . 15
8382ad2antll 710 . . . . . . . . . . . . . 14
8481, 83ffvelrnd 5871 . . . . . . . . . . . . 13
8579, 84eqeltrd 2510 . . . . . . . . . . . 12
86 opelxpi 4910 . . . . . . . . . . . 12
8777, 85, 86syl2anc 643 . . . . . . . . . . 11
8887rexlimiva 2825 . . . . . . . . . 10
8971, 88syl 16 . . . . . . . . 9
9089ex 424 . . . . . . . 8
9170, 90syl5bi 209 . . . . . . 7
92 fvex 5742 . . . . . . . . . 10
93 fvex 5742 . . . . . . . . . 10
9492, 93opth 4435 . . . . . . . . 9
95 simpr 448 . . . . . . . . . . . . . . 15
9695fveq2d 5732 . . . . . . . . . . . . . 14
9796fveq1d 5730 . . . . . . . . . . . . 13
9897eqeq2d 2447 . . . . . . . . . . . 12
99 djussxp 5018 . . . . . . . . . . . . . . . . . 18
10067, 99eqsstri 3378 . . . . . . . . . . . . . . . . 17
101 simprl 733 . . . . . . . . . . . . . . . . 17
102100, 101sseldi 3346 . . . . . . . . . . . . . . . 16
103102adantr 452 . . . . . . . . . . . . . . 15
104 xp1st 6376 . . . . . . . . . . . . . . 15
105103, 104syl 16 . . . . . . . . . . . . . 14
106 simpll 731 . . . . . . . . . . . . . 14
107 nfcv 2572 . . . . . . . . . . . . . . . 16
108 nfcsb1v 3283 . . . . . . . . . . . . . . . 16
109107, 108, 28nff1 5637 . . . . . . . . . . . . . . 15
110 fveq2 5728 . . . . . . . . . . . . . . . . 17
111 f1eq1 5634 . . . . . . . . . . . . . . . . 17
112110, 111syl 16 . . . . . . . . . . . . . . . 16
113 csbeq1a 3259 . . . . . . . . . . . . . . . . 17
114 f1eq2 5635 . . . . . . . . . . . . . . . . 17
115113, 114syl 16 . . . . . . . . . . . . . . . 16
116112, 115bitrd 245 . . . . . . . . . . . . . . 15
117109, 116rspc 3046 . . . . . . . . . . . . . 14
118105, 106, 117sylc 58 . . . . . . . . . . . . 13
119108nfel2 2584 . . . . . . . . . . . . . . . . . . . 20
12075eqcomd 2441 . . . . . . . . . . . . . . . . . . . . . . 23
121120, 113syl 16 . . . . . . . . . . . . . . . . . . . . . 22
12283, 121eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . 21
123122ex 424 . . . . . . . . . . . . . . . . . . . 20
124119, 123rexlimi 2823 . . . . . . . . . . . . . . . . . . 19
12571, 124syl 16 . . . . . . . . . . . . . . . . . 18
126125ex 424 . . . . . . . . . . . . . . . . 17
12770, 126syl5bi 209 . . . . . . . . . . . . . . . 16
128127imp 419 . . . . . . . . . . . . . . 15
129128adantrr 698 . . . . . . . . . . . . . 14
130129adantr 452 . . . . . . . . . . . . 13
131127ralrimiv 2788 . . . . . . . . . . . . . . . . 17
132 fveq2 5728 . . . . . . . . . . . . . . . . . . 19
133 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20
134133csbeq1d 3257 . . . . . . . . . . . . . . . . . . 19
135132, 134eleq12d 2504 . . . . . . . . . . . . . . . . . 18
136135rspccva 3051 . . . . . . . . . . . . . . . . 17
137131, 136sylan 458 . . . . . . . . . . . . . . . 16
138137adantrl 697 . . . . . . . . . . . . . . 15
139138adantr 452 . . . . . . . . . . . . . 14
14095csbeq1d 3257 . . . . . . . . . . . . . 14
141139, 140eleqtrrd 2513 . . . . . . . . . . . . 13
142 f1fveq 6008 . . . . . . . . . . . . 13
143118, 130, 141, 142syl12anc 1182 . . . . . . . . . . . 12
14498, 143bitr3d 247 . . . . . . . . . . 11
145144pm5.32da 623 . . . . . . . . . 10
146 simprr 734 . . . . . . . . . . . 12
147100, 146sseldi 3346 . . . . . . . . . . 11
148 xpopth 6388 . . . . . . . . . . 11
149102, 147, 148syl2anc 643 . . . . . . . . . 10
150145, 149bitrd 245 . . . . . . . . 9
15194, 150syl5bb 249 . . . . . . . 8
152151ex 424 . . . . . . 7
15391, 152dom2d 7148 . . . . . 6
15466, 153syl5com 28 . . . . 5
15549, 154syl5bir 210 . . . 4