Metamath Proof Explorer

Theorem carduni

Description: The union of a set of cardinals is a cardinal. Theorem 18.14 of Monk1 p. 133. (Contributed by Mario Carneiro, 20-Jan-2013)

Ref Expression
Assertion carduni 
|- ( A e. V -> ( A. x e. A ( card ` x ) = x -> ( card ` U. A ) = U. A ) )

Proof

Step Hyp Ref Expression
1 ssonuni 
 |-  ( A e. V -> ( A C_ On -> U. A e. On ) )
2 fveq2 
 |-  ( x = y -> ( card ` x ) = ( card ` y ) )
3 id 
 |-  ( x = y -> x = y )
4 2 3 eqeq12d 
 |-  ( x = y -> ( ( card ` x ) = x <-> ( card ` y ) = y ) )
5 4 rspcv 
 |-  ( y e. A -> ( A. x e. A ( card ` x ) = x -> ( card ` y ) = y ) )
6 cardon 
 |-  ( card ` y ) e. On
7 eleq1 
 |-  ( ( card ` y ) = y -> ( ( card ` y ) e. On <-> y e. On ) )
8 6 7 mpbii 
 |-  ( ( card ` y ) = y -> y e. On )
9 5 8 syl6com 
 |-  ( A. x e. A ( card ` x ) = x -> ( y e. A -> y e. On ) )
10 9 ssrdv 
 |-  ( A. x e. A ( card ` x ) = x -> A C_ On )
11 1 10 impel 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> U. A e. On )
12 cardonle 
 |-  ( U. A e. On -> ( card ` U. A ) C_ U. A )
13 11 12 syl 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( card ` U. A ) C_ U. A )
14 cardon 
 |-  ( card ` U. A ) e. On
15 14 onirri 
 |-  -. ( card ` U. A ) e. ( card ` U. A )
16 eluni 
 |-  ( ( card ` U. A ) e. U. A <-> E. y ( ( card ` U. A ) e. y /\ y e. A ) )
17 elssuni 
 |-  ( y e. A -> y C_ U. A )
18 ssdomg 
 |-  ( U. A e. On -> ( y C_ U. A -> y ~<_ U. A ) )
19 18 adantl 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y C_ U. A -> y ~<_ U. A ) )
20 17 19 syl5 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> y ~<_ U. A ) )
21 id 
 |-  ( ( card ` y ) = y -> ( card ` y ) = y )
22 onenon 
 |-  ( ( card ` y ) e. On -> ( card ` y ) e. dom card )
23 6 22 ax-mp 
 |-  ( card ` y ) e. dom card
24 21 23 eqeltrrdi 
 |-  ( ( card ` y ) = y -> y e. dom card )
25 onenon 
 |-  ( U. A e. On -> U. A e. dom card )
26 carddom2 
 |-  ( ( y e. dom card /\ U. A e. dom card ) -> ( ( card ` y ) C_ ( card ` U. A ) <-> y ~<_ U. A ) )
27 24 25 26 syl2an 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( ( card ` y ) C_ ( card ` U. A ) <-> y ~<_ U. A ) )
28 20 27 sylibrd 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> ( card ` y ) C_ ( card ` U. A ) ) )
29 sseq1 
 |-  ( ( card ` y ) = y -> ( ( card ` y ) C_ ( card ` U. A ) <-> y C_ ( card ` U. A ) ) )
30 29 adantr 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( ( card ` y ) C_ ( card ` U. A ) <-> y C_ ( card ` U. A ) ) )
31 28 30 sylibd 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> y C_ ( card ` U. A ) ) )
32 ssel 
 |-  ( y C_ ( card ` U. A ) -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) )
33 31 32 syl6 
 |-  ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) )
34 33 ex 
 |-  ( ( card ` y ) = y -> ( U. A e. On -> ( y e. A -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) )
35 34 com3r 
 |-  ( y e. A -> ( ( card ` y ) = y -> ( U. A e. On -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) )
36 5 35 syld 
 |-  ( y e. A -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) )
37 36 com4r 
 |-  ( ( card ` U. A ) e. y -> ( y e. A -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) )
38 37 imp 
 |-  ( ( ( card ` U. A ) e. y /\ y e. A ) -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) )
39 38 exlimiv 
 |-  ( E. y ( ( card ` U. A ) e. y /\ y e. A ) -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) )
40 16 39 sylbi 
 |-  ( ( card ` U. A ) e. U. A -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) )
41 40 com13 
 |-  ( U. A e. On -> ( A. x e. A ( card ` x ) = x -> ( ( card ` U. A ) e. U. A -> ( card ` U. A ) e. ( card ` U. A ) ) ) )
42 41 imp 
 |-  ( ( U. A e. On /\ A. x e. A ( card ` x ) = x ) -> ( ( card ` U. A ) e. U. A -> ( card ` U. A ) e. ( card ` U. A ) ) )
43 11 42 sylancom 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( ( card ` U. A ) e. U. A -> ( card ` U. A ) e. ( card ` U. A ) ) )
44 15 43 mtoi 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> -. ( card ` U. A ) e. U. A )
45 14 onordi 
 |-  Ord ( card ` U. A )
46 eloni 
 |-  ( U. A e. On -> Ord U. A )
47 11 46 syl 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> Ord U. A )
48 ordtri4 
 |-  ( ( Ord ( card ` U. A ) /\ Ord U. A ) -> ( ( card ` U. A ) = U. A <-> ( ( card ` U. A ) C_ U. A /\ -. ( card ` U. A ) e. U. A ) ) )
49 45 47 48 sylancr 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( ( card ` U. A ) = U. A <-> ( ( card ` U. A ) C_ U. A /\ -. ( card ` U. A ) e. U. A ) ) )
50 13 44 49 mpbir2and 
 |-  ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( card ` U. A ) = U. A )
51 50 ex 
 |-  ( A e. V -> ( A. x e. A ( card ` x ) = x -> ( card ` U. A ) = U. A ) )