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

Theorem iundom2g 8309
 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 7016 . . . . . . . . 9
43adantl 452 . . . . . . . 8
5 f1f 5543 . . . . . . . . . . . 12
6 reldom 7012 . . . . . . . . . . . . . . 15
76brrelex2i 4833 . . . . . . . . . . . . . 14
86brrelexi 4832 . . . . . . . . . . . . . 14
9 elmapg 6928 . . . . . . . . . . . . . 14
107, 8, 9syl2anc 642 . . . . . . . . . . . . 13
1110adantl 452 . . . . . . . . . . . 12
125, 11syl5ibr 212 . . . . . . . . . . 11
13 ssiun2 4047 . . . . . . . . . . . . 13
1413adantr 451 . . . . . . . . . . . 12
1514sseld 3265 . . . . . . . . . . 11
1612, 15syld 40 . . . . . . . . . 10
1716ancrd 537 . . . . . . . . 9
1817eximdv 1627 . . . . . . . 8
194, 18mpd 14 . . . . . . 7
20 df-rex 2634 . . . . . . 7
2119, 20sylibr 203 . . . . . 6
2221ralimiaa 2702 . . . . 5
232, 22syl 15 . . . 4
24 nfv 1624 . . . . 5
25 nfiu1 4035 . . . . . 6
26 nfcv 2502 . . . . . . 7
27 nfcsb1v 3199 . . . . . . 7
28 nfcv 2502 . . . . . . 7
2926, 27, 28nff1 5541 . . . . . 6
3025, 29nfrex 2683 . . . . 5
31 csbeq1a 3175 . . . . . . 7
32 f1eq2 5539 . . . . . . 7
3331, 32syl 15 . . . . . 6
3433rexbidv 2649 . . . . 5
3524, 30, 34cbvral 2845 . . . 4
3623, 35sylib 188 . . 3
37 f1eq1 5538 . . . 4
3837acni3 7821 . . 3 AC
391, 36, 38syl2anc 642 . 2
40 nfv 1624 . . . . . 6
41 nfcv 2502 . . . . . . 7
4241, 27, 28nff1 5541 . . . . . 6
43 fveq2 5632 . . . . . . . 8
44 f1eq1 5538 . . . . . . . 8
4543, 44syl 15 . . . . . . 7
46 f1eq2 5539 . . . . . . . 8
4731, 46syl 15 . . . . . . 7
4845, 47bitrd 244 . . . . . 6
4940, 42, 48cbvral 2845 . . . . 5
50 df-ne 2531 . . . . . . . 8
51 acnrcl 7816 . . . . . . . . . 10 AC
521, 51syl 15 . . . . . . . . 9
53 r19.2z 3632 . . . . . . . . . . . 12
547rexlimivw 2748 . . . . . . . . . . . 12
5553, 54syl 15 . . . . . . . . . . 11
5655expcom 424 . . . . . . . . . 10
572, 56syl 15 . . . . . . . . 9
58 xpexg 4903 . . . . . . . . 9
5952, 57, 58ee12an 1368 . . . . . . . 8
6050, 59syl5bir 209 . . . . . . 7
61 xpeq1 4806 . . . . . . . 8
62 xp0r 4871 . . . . . . . . 9
63 0ex 4252 . . . . . . . . 9
6462, 63eqeltri 2436 . . . . . . . 8
6561, 64syl6eqel 2454 . . . . . . 7
6660, 65pm2.61d2 152 . . . . . 6
67 iunfo.1 . . . . . . . . . 10
6867eleq2i 2430 . . . . . . . . 9
69 eliun 4011 . . . . . . . . 9
7068, 69bitri 240 . . . . . . . 8
71 r19.29 2768 . . . . . . . . . 10
72 xp1st 6276 . . . . . . . . . . . . . . 15
7372ad2antll 709 . . . . . . . . . . . . . 14
74 elsni 3753 . . . . . . . . . . . . . 14
7573, 74syl 15 . . . . . . . . . . . . 13
76 simpl 443 . . . . . . . . . . . . 13
7775, 76eqeltrd 2440 . . . . . . . . . . . 12
7875fveq2d 5636 . . . . . . . . . . . . . 14
7978fveq1d 5634 . . . . . . . . . . . . 13
80 f1f 5543 . . . . . . . . . . . . . . 15
8180ad2antrl 708 . . . . . . . . . . . . . 14
82 xp2nd 6277 . . . . . . . . . . . . . . 15
8382ad2antll 709 . . . . . . . . . . . . . 14
84 ffvelrn 5770 . . . . . . . . . . . . . 14
8581, 83, 84syl2anc 642 . . . . . . . . . . . . 13
8679, 85eqeltrd 2440 . . . . . . . . . . . 12
87 opelxpi 4824 . . . . . . . . . . . 12
8877, 86, 87syl2anc 642 . . . . . . . . . . 11
8988rexlimiva 2747 . . . . . . . . . 10
9071, 89syl 15 . . . . . . . . 9
9190ex 423 . . . . . . . 8
9270, 91syl5bi 208 . . . . . . 7
93 fvex 5646 . . . . . . . . . 10
94 fvex 5646 . . . . . . . . . 10
9593, 94opth 4348 . . . . . . . . 9
96 simpr 447 . . . . . . . . . . . . . . 15
9796fveq2d 5636 . . . . . . . . . . . . . 14
9897fveq1d 5634 . . . . . . . . . . . . 13
9998eqeq2d 2377 . . . . . . . . . . . 12
100 djussxp 4932 . . . . . . . . . . . . . . . . . 18
10167, 100eqsstri 3294 . . . . . . . . . . . . . . . . 17
102 simprl 732 . . . . . . . . . . . . . . . . 17
103101, 102sseldi 3264 . . . . . . . . . . . . . . . 16
104103adantr 451 . . . . . . . . . . . . . . 15
105 xp1st 6276 . . . . . . . . . . . . . . 15
106104, 105syl 15 . . . . . . . . . . . . . 14
107 simpll 730 . . . . . . . . . . . . . 14
108 nfcv 2502 . . . . . . . . . . . . . . . 16
109 nfcsb1v 3199 . . . . . . . . . . . . . . . 16
110108, 109, 28nff1 5541 . . . . . . . . . . . . . . 15
111 fveq2 5632 . . . . . . . . . . . . . . . . 17
112 f1eq1 5538 . . . . . . . . . . . . . . . . 17
113111, 112syl 15 . . . . . . . . . . . . . . . 16
114 csbeq1a 3175 . . . . . . . . . . . . . . . . 17
115 f1eq2 5539 . . . . . . . . . . . . . . . . 17
116114, 115syl 15 . . . . . . . . . . . . . . . 16
117113, 116bitrd 244 . . . . . . . . . . . . . . 15
118110, 117rspc 2963 . . . . . . . . . . . . . 14
119106, 107, 118sylc 56 . . . . . . . . . . . . 13
120109nfel2 2514 . . . . . . . . . . . . . . . . . . . 20
12175eqcomd 2371 . . . . . . . . . . . . . . . . . . . . . . 23
122121, 114syl 15 . . . . . . . . . . . . . . . . . . . . . 22
12383, 122eleqtrd 2442 . . . . . . . . . . . . . . . . . . . . 21
124123ex 423 . . . . . . . . . . . . . . . . . . . 20
125120, 124rexlimi 2745 . . . . . . . . . . . . . . . . . . 19
12671, 125syl 15 . . . . . . . . . . . . . . . . . 18
127126ex 423 . . . . . . . . . . . . . . . . 17
12870, 127syl5bi 208 . . . . . . . . . . . . . . . 16
129128imp 418 . . . . . . . . . . . . . . 15
130129adantrr 697 . . . . . . . . . . . . . 14
131130adantr 451 . . . . . . . . . . . . 13
132128ralrimiv 2710 . . . . . . . . . . . . . . . . 17
133 fveq2 5632 . . . . . . . . . . . . . . . . . . 19
134 fveq2 5632 . . . . . . . . . . . . . . . . . . . 20
135134csbeq1d 3173 . . . . . . . . . . . . . . . . . . 19
136133, 135eleq12d 2434 . . . . . . . . . . . . . . . . . 18
137136rspccva 2968 . . . . . . . . . . . . . . . . 17
138132, 137sylan 457 . . . . . . . . . . . . . . . 16
139138adantrl 696 . . . . . . . . . . . . . . 15
140139adantr 451 . . . . . . . . . . . . . 14
14196csbeq1d 3173 . . . . . . . . . . . . . 14
142140, 141eleqtrrd 2443 . . . . . . . . . . . . 13
143 f1fveq 5908 . . . . . . . . . . . . 13
144119, 131, 142, 143syl12anc 1181 . . . . . . . . . . . 12
14599, 144bitr3d 246 . . . . . . . . . . 11
146145pm5.32da 622 . . . . . . . . . 10
147 simprr 733 . . . . . . . . . . . 12
148101, 147sseldi 3264 . . . . . . . . . . 11
149 xpopth 6288 . . . . . . . . . . 11
150103, 148, 149syl2anc 642 . . . . . . . . . 10
151146, 150bitrd 244 . . . . . . . . 9
15295, 151syl5bb 248 . . . . . . . 8
153152ex 423 . . . . . . 7
15492, 153dom2d 7045 . . . . . 6
15566, 154syl5com 26 . . . . 5
15649, 155syl5bir 209 . . . 4
157156adantld 453 . . 3
158157exlimdv 1641 . 2
15939, 158mpd 14 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358  wex 1546   wceq 1647   wcel 1715   wne 2529  wral 2628  wrex 2629  cvv 2873  csb 3167   wss 3238  c0 3543  csn 3729  cop 3732  ciun 4007   class class class wbr 4125   cxp 4790  wf 5354  wf1 5355  cfv 5358  (class class class)co 5981  c1st 6247  c2nd 6248   cmap 6915   cdom 7004  AC wacn 7718 This theorem is referenced by:  iundomg  8310  iundom  8311 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-1st 6249  df-2nd 6250  df-map 6917  df-dom 7008  df-acn 7722
 Copyright terms: Public domain W3C validator