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∈V→∀x∈Acard⁡x=x→card⁡⋃A=⋃A

Proof

Step Hyp Ref Expression
1 ssonuni ⊢A∈V→A⊆On→⋃A∈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∈A→∀x∈Acard⁡x=x→card⁡y=y
6 cardon ⊢card⁡y∈On
7 eleq1 ⊢card⁡y=y→card⁡y∈On↔y∈On
8 6 7 mpbii ⊢card⁡y=y→y∈On
9 5 8 syl6com ⊢∀x∈Acard⁡x=x→y∈A→y∈On
10 9 ssrdv ⊢∀x∈Acard⁡x=x→A⊆On
11 1 10 impel ⊢A∈V∧∀x∈Acard⁡x=x→⋃A∈On
12 cardonle ⊢⋃A∈On→card⁡⋃A⊆⋃A
13 11 12 syl ⊢A∈V∧∀x∈Acard⁡x=x→card⁡⋃A⊆⋃A
14 cardon ⊢card⁡⋃A∈On
15 14 onirri ⊢¬card⁡⋃A∈card⁡⋃A
16 eluni ⊢card⁡⋃A∈⋃A↔∃ycard⁡⋃A∈y∧y∈A
17 elssuni ⊢y∈A→y⊆⋃A
18 ssdomg ⊢⋃A∈On→y⊆⋃A→y≼⋃A
19 18 adantl ⊢card⁡y=y∧⋃A∈On→y⊆⋃A→y≼⋃A
20 17 19 syl5 ⊢card⁡y=y∧⋃A∈On→y∈A→y≼⋃A
21 id ⊢card⁡y=y→card⁡y=y
22 onenon ⊢card⁡y∈On→card⁡y∈dom⁡card
23 6 22 ax-mp ⊢card⁡y∈dom⁡card
24 21 23 eqeltrrdi ⊢card⁡y=y→y∈dom⁡card
25 onenon ⊢⋃A∈On→⋃A∈dom⁡card
26 carddom2 ⊢y∈dom⁡card∧⋃A∈dom⁡card→card⁡y⊆card⁡⋃A↔y≼⋃A
27 24 25 26 syl2an ⊢card⁡y=y∧⋃A∈On→card⁡y⊆card⁡⋃A↔y≼⋃A
28 20 27 sylibrd ⊢card⁡y=y∧⋃A∈On→y∈A→card⁡y⊆card⁡⋃A
29 sseq1 ⊢card⁡y=y→card⁡y⊆card⁡⋃A↔y⊆card⁡⋃A
30 29 adantr ⊢card⁡y=y∧⋃A∈On→card⁡y⊆card⁡⋃A↔y⊆card⁡⋃A
31 28 30 sylibd ⊢card⁡y=y∧⋃A∈On→y∈A→y⊆card⁡⋃A
32 ssel ⊢y⊆card⁡⋃A→card⁡⋃A∈y→card⁡⋃A∈card⁡⋃A
33 31 32 syl6 ⊢card⁡y=y∧⋃A∈On→y∈A→card⁡⋃A∈y→card⁡⋃A∈card⁡⋃A
34 33 ex ⊢card⁡y=y→⋃A∈On→y∈A→card⁡⋃A∈y→card⁡⋃A∈card⁡⋃A
35 34 com3r ⊢y∈A→card⁡y=y→⋃A∈On→card⁡⋃A∈y→card⁡⋃A∈card⁡⋃A
36 5 35 syld ⊢y∈A→∀x∈Acard⁡x=x→⋃A∈On→card⁡⋃A∈y→card⁡⋃A∈card⁡⋃A
37 36 com4r ⊢card⁡⋃A∈y→y∈A→∀x∈Acard⁡x=x→⋃A∈On→card⁡⋃A∈card⁡⋃A
38 37 imp ⊢card⁡⋃A∈y∧y∈A→∀x∈Acard⁡x=x→⋃A∈On→card⁡⋃A∈card⁡⋃A
39 38 exlimiv ⊢∃ycard⁡⋃A∈y∧y∈A→∀x∈Acard⁡x=x→⋃A∈On→card⁡⋃A∈card⁡⋃A
40 16 39 sylbi ⊢card⁡⋃A∈⋃A→∀x∈Acard⁡x=x→⋃A∈On→card⁡⋃A∈card⁡⋃A
41 40 com13 ⊢⋃A∈On→∀x∈Acard⁡x=x→card⁡⋃A∈⋃A→card⁡⋃A∈card⁡⋃A
42 41 imp ⊢⋃A∈On∧∀x∈Acard⁡x=x→card⁡⋃A∈⋃A→card⁡⋃A∈card⁡⋃A
43 11 42 sylancom ⊢A∈V∧∀x∈Acard⁡x=x→card⁡⋃A∈⋃A→card⁡⋃A∈card⁡⋃A
44 15 43 mtoi ⊢A∈V∧∀x∈Acard⁡x=x→¬card⁡⋃A∈⋃A
45 14 onordi ⊢Ord⁡card⁡⋃A
46 eloni ⊢⋃A∈On→Ord⁡⋃A
47 11 46 syl ⊢A∈V∧∀x∈Acard⁡x=x→Ord⁡⋃A
48 ordtri4 ⊢Ord⁡card⁡⋃A∧Ord⁡⋃A→card⁡⋃A=⋃A↔card⁡⋃A⊆⋃A∧¬card⁡⋃A∈⋃A
49 45 47 48 sylancr ⊢A∈V∧∀x∈Acard⁡x=x→card⁡⋃A=⋃A↔card⁡⋃A⊆⋃A∧¬card⁡⋃A∈⋃A
50 13 44 49 mpbir2and ⊢A∈V∧∀x∈Acard⁡x=x→card⁡⋃A=⋃A
51 50 ex ⊢A∈V→∀x∈Acard⁡x=x→card⁡⋃A=⋃A