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 ∈ A card ⁡ 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 ∈ A card ⁡ 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 ∈ A card ⁡ x = x → y ∈ A → y ∈ On
10 9 ssrdv ⊢ ∀ x ∈ A card ⁡ x = x → A ⊆ On
11 1 10 impel ⊢ A ∈ V ∧ ∀ x ∈ A card ⁡ x = x → ⋃ A ∈ On
12 cardonle ⊢ ⋃ A ∈ On → card ⁡ ⋃ A ⊆ ⋃ A
13 11 12 syl ⊢ A ∈ V ∧ ∀ x ∈ A card ⁡ x = x → card ⁡ ⋃ A ⊆ ⋃ A
14 cardon ⊢ card ⁡ ⋃ A ∈ On
15 14 onirri ⊢ ¬ card ⁡ ⋃ A ∈ card ⁡ ⋃ A
16 eluni ⊢ card ⁡ ⋃ A ∈ ⋃ A ↔ ∃ y card ⁡ ⋃ 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 ∈ A card ⁡ x = x → ⋃ A ∈ On → card ⁡ ⋃ A ∈ y → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
37 36 com4r ⊢ card ⁡ ⋃ A ∈ y → y ∈ A → ∀ x ∈ A card ⁡ x = x → ⋃ A ∈ On → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
38 37 imp ⊢ card ⁡ ⋃ A ∈ y ∧ y ∈ A → ∀ x ∈ A card ⁡ x = x → ⋃ A ∈ On → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
39 38 exlimiv ⊢ ∃ y card ⁡ ⋃ A ∈ y ∧ y ∈ A → ∀ x ∈ A card ⁡ x = x → ⋃ A ∈ On → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
40 16 39 sylbi ⊢ card ⁡ ⋃ A ∈ ⋃ A → ∀ x ∈ A card ⁡ x = x → ⋃ A ∈ On → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
41 40 com13 ⊢ ⋃ A ∈ On → ∀ x ∈ A card ⁡ x = x → card ⁡ ⋃ A ∈ ⋃ A → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
42 41 imp ⊢ ⋃ A ∈ On ∧ ∀ x ∈ A card ⁡ x = x → card ⁡ ⋃ A ∈ ⋃ A → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
43 11 42 sylancom ⊢ A ∈ V ∧ ∀ x ∈ A card ⁡ x = x → card ⁡ ⋃ A ∈ ⋃ A → card ⁡ ⋃ A ∈ card ⁡ ⋃ A
44 15 43 mtoi ⊢ A ∈ V ∧ ∀ x ∈ A card ⁡ x = x → ¬ card ⁡ ⋃ A ∈ ⋃ A
45 14 onordi ⊢ Ord ⁡ card ⁡ ⋃ A
46 eloni ⊢ ⋃ A ∈ On → Ord ⁡ ⋃ A
47 11 46 syl ⊢ A ∈ V ∧ ∀ x ∈ A card ⁡ 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 ∈ A card ⁡ x = x → card ⁡ ⋃ A = ⋃ A ↔ card ⁡ ⋃ A ⊆ ⋃ A ∧ ¬ card ⁡ ⋃ A ∈ ⋃ A
50 13 44 49 mpbir2and ⊢ A ∈ V ∧ ∀ x ∈ A card ⁡ x = x → card ⁡ ⋃ A = ⋃ A
51 50 ex ⊢ A ∈ V → ∀ x ∈ A card ⁡ x = x → card ⁡ ⋃ A = ⋃ A