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

Theorem iundom2g 8904
 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 7517 . . . . . . . . 9
43adantl 466 . . . . . . . 8
5 f1f 5772 . . . . . . . . . . . 12
6 reldom 7512 . . . . . . . . . . . . . . 15
76brrelex2i 5033 . . . . . . . . . . . . . 14
86brrelexi 5032 . . . . . . . . . . . . . 14
9 elmapg 7423 . . . . . . . . . . . . . 14
107, 8, 9syl2anc 661 . . . . . . . . . . . . 13
1110adantl 466 . . . . . . . . . . . 12
125, 11syl5ibr 221 . . . . . . . . . . 11
13 ssiun2 4361 . . . . . . . . . . . . 13
1413adantr 465 . . . . . . . . . . . 12
1514sseld 3496 . . . . . . . . . . 11
1612, 15syld 44 . . . . . . . . . 10
1716ancrd 554 . . . . . . . . 9
1817eximdv 1681 . . . . . . . 8
194, 18mpd 15 . . . . . . 7
20 df-rex 2813 . . . . . . 7
2119, 20sylibr 212 . . . . . 6
2221ralimiaa 2849 . . . . 5
232, 22syl 16 . . . 4
24 nfv 1678 . . . . 5
25 nfiu1 4348 . . . . . 6
26 nfcv 2622 . . . . . . 7
27 nfcsb1v 3444 . . . . . . 7
28 nfcv 2622 . . . . . . 7
2926, 27, 28nff1 5770 . . . . . 6
3025, 29nfrex 2920 . . . . 5
31 csbeq1a 3437 . . . . . . 7
32 f1eq2 5768 . . . . . . 7
3331, 32syl 16 . . . . . 6
3433rexbidv 2966 . . . . 5
3524, 30, 34cbvral 3077 . . . 4
3623, 35sylib 196 . . 3
37 f1eq1 5767 . . . 4
3837acni3 8417 . . 3 AC
391, 36, 38syl2anc 661 . 2
40 nfv 1678 . . . . . 6
41 nfcv 2622 . . . . . . 7
4241, 27, 28nff1 5770 . . . . . 6
43 fveq2 5857 . . . . . . . 8
44 f1eq1 5767 . . . . . . . 8
4543, 44syl 16 . . . . . . 7
46 f1eq2 5768 . . . . . . . 8
4731, 46syl 16 . . . . . . 7
4845, 47bitrd 253 . . . . . 6
4940, 42, 48cbvral 3077 . . . . 5
50 df-ne 2657 . . . . . . . 8
51 acnrcl 8412 . . . . . . . . . 10 AC
521, 51syl 16 . . . . . . . . 9
53 r19.2z 3910 . . . . . . . . . . . 12
547rexlimivw 2945 . . . . . . . . . . . 12
5553, 54syl 16 . . . . . . . . . . 11
5655expcom 435 . . . . . . . . . 10
572, 56syl 16 . . . . . . . . 9
58 xpexg 6702 . . . . . . . . 9
5952, 57, 58syl6an 545 . . . . . . . 8
6050, 59syl5bir 218 . . . . . . 7
61 xpeq1 5006 . . . . . . . 8
62 0xp 5071 . . . . . . . . 9
63 0ex 4570 . . . . . . . . 9
6462, 63eqeltri 2544 . . . . . . . 8
6561, 64syl6eqel 2556 . . . . . . 7
6660, 65pm2.61d2 160 . . . . . 6
67 iunfo.1 . . . . . . . . . 10
6867eleq2i 2538 . . . . . . . . 9
69 eliun 4323 . . . . . . . . 9
7068, 69bitri 249 . . . . . . . 8
71 r19.29 2990 . . . . . . . . . 10
72 xp1st 6804 . . . . . . . . . . . . . . 15
7372ad2antll 728 . . . . . . . . . . . . . 14
74 elsni 4045 . . . . . . . . . . . . . 14
7573, 74syl 16 . . . . . . . . . . . . 13
76 simpl 457 . . . . . . . . . . . . 13
7775, 76eqeltrd 2548 . . . . . . . . . . . 12
7875fveq2d 5861 . . . . . . . . . . . . . 14
7978fveq1d 5859 . . . . . . . . . . . . 13
80 f1f 5772 . . . . . . . . . . . . . . 15
8180ad2antrl 727 . . . . . . . . . . . . . 14
82 xp2nd 6805 . . . . . . . . . . . . . . 15
8382ad2antll 728 . . . . . . . . . . . . . 14
8481, 83ffvelrnd 6013 . . . . . . . . . . . . 13
8579, 84eqeltrd 2548 . . . . . . . . . . . 12
86 opelxpi 5023 . . . . . . . . . . . 12
8777, 85, 86syl2anc 661 . . . . . . . . . . 11
8887rexlimiva 2944 . . . . . . . . . 10
8971, 88syl 16 . . . . . . . . 9
9089ex 434 . . . . . . . 8
9170, 90syl5bi 217 . . . . . . 7
92 fvex 5867 . . . . . . . . . 10
93 fvex 5867 . . . . . . . . . 10
9492, 93opth 4714 . . . . . . . . 9
95 simpr 461 . . . . . . . . . . . . . . 15
9695fveq2d 5861 . . . . . . . . . . . . . 14
9796fveq1d 5859 . . . . . . . . . . . . 13
9897eqeq2d 2474 . . . . . . . . . . . 12
99 djussxp 5139 . . . . . . . . . . . . . . . . . 18
10067, 99eqsstri 3527 . . . . . . . . . . . . . . . . 17
101 simprl 755 . . . . . . . . . . . . . . . . 17
102100, 101sseldi 3495 . . . . . . . . . . . . . . . 16
103102adantr 465 . . . . . . . . . . . . . . 15
104 xp1st 6804 . . . . . . . . . . . . . . 15
105103, 104syl 16 . . . . . . . . . . . . . 14
106 simpll 753 . . . . . . . . . . . . . 14
107 nfcv 2622 . . . . . . . . . . . . . . . 16
108 nfcsb1v 3444 . . . . . . . . . . . . . . . 16
109107, 108, 28nff1 5770 . . . . . . . . . . . . . . 15
110 fveq2 5857 . . . . . . . . . . . . . . . . 17
111 f1eq1 5767 . . . . . . . . . . . . . . . . 17
112110, 111syl 16 . . . . . . . . . . . . . . . 16
113 csbeq1a 3437 . . . . . . . . . . . . . . . . 17
114 f1eq2 5768 . . . . . . . . . . . . . . . . 17
115113, 114syl 16 . . . . . . . . . . . . . . . 16
116112, 115bitrd 253 . . . . . . . . . . . . . . 15
117109, 116rspc 3201 . . . . . . . . . . . . . 14
118105, 106, 117sylc 60 . . . . . . . . . . . . 13
119108nfel2 2640 . . . . . . . . . . . . . . . . . . . 20
12075eqcomd 2468 . . . . . . . . . . . . . . . . . . . . . . 23
121120, 113syl 16 . . . . . . . . . . . . . . . . . . . . . 22
12283, 121eleqtrd 2550 . . . . . . . . . . . . . . . . . . . . 21
123122ex 434 . . . . . . . . . . . . . . . . . . . 20
124119, 123rexlimi 2938 . . . . . . . . . . . . . . . . . . 19
12571, 124syl 16 . . . . . . . . . . . . . . . . . 18
126125ex 434 . . . . . . . . . . . . . . . . 17
12770, 126syl5bi 217 . . . . . . . . . . . . . . . 16
128127imp 429 . . . . . . . . . . . . . . 15
129128adantrr 716 . . . . . . . . . . . . . 14
130129adantr 465 . . . . . . . . . . . . 13
131127ralrimiv 2869 . . . . . . . . . . . . . . . . 17
132 fveq2 5857 . . . . . . . . . . . . . . . . . . 19
133 fveq2 5857 . . . . . . . . . . . . . . . . . . . 20
134133csbeq1d 3435 . . . . . . . . . . . . . . . . . . 19
135132, 134eleq12d 2542 . . . . . . . . . . . . . . . . . 18
136135rspccva 3206 . . . . . . . . . . . . . . . . 17
137131, 136sylan 471 . . . . . . . . . . . . . . . 16
138137adantrl 715 . . . . . . . . . . . . . . 15
139138adantr 465 . . . . . . . . . . . . . 14
14095csbeq1d 3435 . . . . . . . . . . . . . 14
141139, 140eleqtrrd 2551 . . . . . . . . . . . . 13
142 f1fveq 6149 . . . . . . . . . . . . 13
143118, 130, 141, 142syl12anc 1221 . . . . . . . . . . . 12
14498, 143bitr3d 255 . . . . . . . . . . 11
145144pm5.32da 641 . . . . . . . . . 10
146 simprr 756 . . . . . . . . . . . 12
147100, 146sseldi 3495 . . . . . . . . . . 11
148 xpopth 6813 . . . . . . . . . . 11
149102, 147, 148syl2anc 661 . . . . . . . . . 10
150145, 149bitrd 253 . . . . . . . . 9
15194, 150syl5bb 257 . . . . . . . 8
152151ex 434 . . . . . . 7
15391, 152dom2d 7546 . . . . . 6
15466, 153syl5com 30 . . . . 5
15549, 154syl5bir 218 . . . 4
156155adantld 467 . . 3
157156exlimdv 1695 . 2
15839, 157mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   wceq 1374  wex 1591   wcel 1762   wne 2655  wral 2807  wrex 2808  cvv 3106  csb 3428   wss 3469  c0 3778  csn 4020  cop 4026  ciun 4318   class class class wbr 4440   cxp 4990  wf 5575  wf1 5576  cfv 5579  (class class class)co 6275  c1st 6772  c2nd 6773   cmap 7410   cdom 7504  AC wacn 8308 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6774  df-2nd 6775  df-map 7412  df-dom 7508  df-acn 8312 This theorem is referenced by:  iundomg  8905  iundom  8906
 Copyright terms: Public domain W3C validator