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 ) )