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

Theorem iundom2g 8983
 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 7598 . . . . . . . . 9
43adantl 473 . . . . . . . 8
5 f1f 5792 . . . . . . . . . . . 12
6 reldom 7593 . . . . . . . . . . . . . . 15
76brrelex2i 4881 . . . . . . . . . . . . . 14
86brrelexi 4880 . . . . . . . . . . . . . 14
97, 8elmapd 7504 . . . . . . . . . . . . 13
109adantl 473 . . . . . . . . . . . 12
115, 10syl5ibr 229 . . . . . . . . . . 11
12 ssiun2 4312 . . . . . . . . . . . . 13
1312adantr 472 . . . . . . . . . . . 12
1413sseld 3417 . . . . . . . . . . 11
1511, 14syld 44 . . . . . . . . . 10
1615ancrd 563 . . . . . . . . 9
1716eximdv 1772 . . . . . . . 8
184, 17mpd 15 . . . . . . 7
19 df-rex 2762 . . . . . . 7
2018, 19sylibr 217 . . . . . 6
2120ralimiaa 2795 . . . . 5
222, 21syl 17 . . . 4
23 nfv 1769 . . . . 5
24 nfiu1 4299 . . . . . 6
25 nfcv 2612 . . . . . . 7
26 nfcsb1v 3365 . . . . . . 7
27 nfcv 2612 . . . . . . 7
2825, 26, 27nff1 5790 . . . . . 6
2924, 28nfrex 2848 . . . . 5
30 csbeq1a 3358 . . . . . . 7
31 f1eq2 5788 . . . . . . 7
3230, 31syl 17 . . . . . 6
3332rexbidv 2892 . . . . 5
3423, 29, 33cbvral 3001 . . . 4
3522, 34sylib 201 . . 3
36 f1eq1 5787 . . . 4
3736acni3 8496 . . 3 AC
381, 35, 37syl2anc 673 . 2
39 nfv 1769 . . . . . 6
40 nfcv 2612 . . . . . . 7
4140, 26, 27nff1 5790 . . . . . 6
42 fveq2 5879 . . . . . . . 8
43 f1eq1 5787 . . . . . . . 8
4442, 43syl 17 . . . . . . 7
45 f1eq2 5788 . . . . . . . 8
4630, 45syl 17 . . . . . . 7
4744, 46bitrd 261 . . . . . 6
4839, 41, 47cbvral 3001 . . . . 5
49 df-ne 2643 . . . . . . . 8
50 acnrcl 8491 . . . . . . . . . 10 AC
511, 50syl 17 . . . . . . . . 9
52 r19.2z 3849 . . . . . . . . . . . 12
537rexlimivw 2869 . . . . . . . . . . . 12
5452, 53syl 17 . . . . . . . . . . 11
5554expcom 442 . . . . . . . . . 10
562, 55syl 17 . . . . . . . . 9
57 xpexg 6612 . . . . . . . . 9
5851, 56, 57syl6an 554 . . . . . . . 8
5949, 58syl5bir 226 . . . . . . 7
60 xpeq1 4853 . . . . . . . 8
61 0xp 4920 . . . . . . . . 9
62 0ex 4528 . . . . . . . . 9
6361, 62eqeltri 2545 . . . . . . . 8
6460, 63syl6eqel 2557 . . . . . . 7
6559, 64pm2.61d2 165 . . . . . 6
66 iunfo.1 . . . . . . . . . 10
6766eleq2i 2541 . . . . . . . . 9
68 eliun 4274 . . . . . . . . 9
6967, 68bitri 257 . . . . . . . 8
70 r19.29 2912 . . . . . . . . . 10
71 xp1st 6842 . . . . . . . . . . . . . . 15
7271ad2antll 743 . . . . . . . . . . . . . 14
73 elsni 3985 . . . . . . . . . . . . . 14
7472, 73syl 17 . . . . . . . . . . . . 13
75 simpl 464 . . . . . . . . . . . . 13
7674, 75eqeltrd 2549 . . . . . . . . . . . 12
7774fveq2d 5883 . . . . . . . . . . . . . 14
7877fveq1d 5881 . . . . . . . . . . . . 13
79 f1f 5792 . . . . . . . . . . . . . . 15
8079ad2antrl 742 . . . . . . . . . . . . . 14
81 xp2nd 6843 . . . . . . . . . . . . . . 15
8281ad2antll 743 . . . . . . . . . . . . . 14
8380, 82ffvelrnd 6038 . . . . . . . . . . . . 13
8478, 83eqeltrd 2549 . . . . . . . . . . . 12
85 opelxpi 4871 . . . . . . . . . . . 12
8676, 84, 85syl2anc 673 . . . . . . . . . . 11
8786rexlimiva 2868 . . . . . . . . . 10
8870, 87syl 17 . . . . . . . . 9
8988ex 441 . . . . . . . 8
9069, 89syl5bi 225 . . . . . . 7
91 fvex 5889 . . . . . . . . . 10
92 fvex 5889 . . . . . . . . . 10
9391, 92opth 4676 . . . . . . . . 9
94 simpr 468 . . . . . . . . . . . . . . 15
9594fveq2d 5883 . . . . . . . . . . . . . 14
9695fveq1d 5881 . . . . . . . . . . . . 13
9796eqeq2d 2481 . . . . . . . . . . . 12
98 djussxp 4985 . . . . . . . . . . . . . . . . . 18
9966, 98eqsstri 3448 . . . . . . . . . . . . . . . . 17
100 simprl 772 . . . . . . . . . . . . . . . . 17
10199, 100sseldi 3416 . . . . . . . . . . . . . . . 16
102101adantr 472 . . . . . . . . . . . . . . 15
103 xp1st 6842 . . . . . . . . . . . . . . 15
104102, 103syl 17 . . . . . . . . . . . . . 14
105 simpll 768 . . . . . . . . . . . . . 14
106 nfcv 2612 . . . . . . . . . . . . . . . 16
107 nfcsb1v 3365 . . . . . . . . . . . . . . . 16
108106, 107, 27nff1 5790 . . . . . . . . . . . . . . 15
109 fveq2 5879 . . . . . . . . . . . . . . . . 17
110 f1eq1 5787 . . . . . . . . . . . . . . . . 17
111109, 110syl 17 . . . . . . . . . . . . . . . 16
112 csbeq1a 3358 . . . . . . . . . . . . . . . . 17
113 f1eq2 5788 . . . . . . . . . . . . . . . . 17
114112, 113syl 17 . . . . . . . . . . . . . . . 16
115111, 114bitrd 261 . . . . . . . . . . . . . . 15
116108, 115rspc 3130 . . . . . . . . . . . . . 14
117104, 105, 116sylc 61 . . . . . . . . . . . . 13
118107nfel2 2628 . . . . . . . . . . . . . . . . . . . 20
11974eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . 23
120119, 112syl 17 . . . . . . . . . . . . . . . . . . . . . 22
12182, 120eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . 21
122121ex 441 . . . . . . . . . . . . . . . . . . . 20
123118, 122rexlimi 2864 . . . . . . . . . . . . . . . . . . 19
12470, 123syl 17 . . . . . . . . . . . . . . . . . 18
125124ex 441 . . . . . . . . . . . . . . . . 17
12669, 125syl5bi 225 . . . . . . . . . . . . . . . 16
127126imp 436 . . . . . . . . . . . . . . 15
128127adantrr 731 . . . . . . . . . . . . . 14
129128adantr 472 . . . . . . . . . . . . 13
130126ralrimiv 2808 . . . . . . . . . . . . . . . . 17
131 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
132 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
133132csbeq1d 3356 . . . . . . . . . . . . . . . . . . 19
134131, 133eleq12d 2543 . . . . . . . . . . . . . . . . . 18
135134rspccva 3135 . . . . . . . . . . . . . . . . 17
136130, 135sylan 479 . . . . . . . . . . . . . . . 16
137136adantrl 730 . . . . . . . . . . . . . . 15
138137adantr 472 . . . . . . . . . . . . . 14
13994csbeq1d 3356 . . . . . . . . . . . . . 14
140138, 139eleqtrrd 2552 . . . . . . . . . . . . 13
141 f1fveq 6181 . . . . . . . . . . . . 13
142117, 129, 140, 141syl12anc 1290 . . . . . . . . . . . 12
14397, 142bitr3d 263 . . . . . . . . . . 11
144143pm5.32da 653 . . . . . . . . . 10
145 simprr 774 . . . . . . . . . . . 12
14699, 145sseldi 3416 . . . . . . . . . . 11
147 xpopth 6851 . . . . . . . . . . 11
148101, 146, 147syl2anc 673 . . . . . . . . . 10
149144, 148bitrd 261 . . . . . . . . 9
15093, 149syl5bb 265 . . . . . . . 8
151150ex 441 . . . . . . 7
15290, 151dom2d 7628 . . . . . 6
15365, 152syl5com 30 . . . . 5
15448, 153syl5bir 226 . . . 4