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

Theorem cardiun 8380
 Description: The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.)
Assertion
Ref Expression
cardiun
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem cardiun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 abrexexg 6774 . . . . . 6
2 vex 3112 . . . . . . . . 9
3 eqeq1 2461 . . . . . . . . . 10
43rexbidv 2968 . . . . . . . . 9
52, 4elab 3246 . . . . . . . 8
6 cardidm 8357 . . . . . . . . . 10
7 fveq2 5872 . . . . . . . . . 10
8 id 22 . . . . . . . . . 10
96, 7, 83eqtr4a 2524 . . . . . . . . 9
109rexlimivw 2946 . . . . . . . 8
115, 10sylbi 195 . . . . . . 7
1211rgen 2817 . . . . . 6
13 carduni 8379 . . . . . 6
141, 12, 13mpisyl 18 . . . . 5
15 fvex 5882 . . . . . . 7
1615dfiun2 4366 . . . . . 6
1716fveq2i 5875 . . . . 5
1814, 17, 163eqtr4g 2523 . . . 4