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 ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( card ‘ ∪ 𝐴 ) = ∪ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssonuni ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )
2 fveq2 ⊢ ( 𝑥 = 𝑦 → ( card ‘ 𝑥 ) = ( card ‘ 𝑦 ) )
3 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
4 2 3 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ 𝑦 ) = 𝑦 ) )
5 4 rspcv ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( card ‘ 𝑦 ) = 𝑦 ) )
6 cardon ⊢ ( card ‘ 𝑦 ) ∈ On
7 eleq1 ⊢ ( ( card ‘ 𝑦 ) = 𝑦 → ( ( card ‘ 𝑦 ) ∈ On ↔ 𝑦 ∈ On ) )
8 6 7 mpbii ⊢ ( ( card ‘ 𝑦 ) = 𝑦 → 𝑦 ∈ On )
9 5 8 syl6com ⊢ ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
10 9 ssrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → 𝐴 ⊆ On )
11 1 10 impel ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ∪ 𝐴 ∈ On )
12 cardonle ⊢ ( ∪ 𝐴 ∈ On → ( card ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 )
13 11 12 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ( card ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 )
14 cardon ⊢ ( card ‘ ∪ 𝐴 ) ∈ On
15 14 onirri ⊢ ¬ ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 )
16 eluni ⊢ ( ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
17 elssuni ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝐴 )
18 ssdomg ⊢ ( ∪ 𝐴 ∈ On → ( 𝑦 ⊆ ∪ 𝐴 → 𝑦 ≼ ∪ 𝐴 ) )
19 18 adantl ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( 𝑦 ⊆ ∪ 𝐴 → 𝑦 ≼ ∪ 𝐴 ) )
20 17 19 syl5 ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 → 𝑦 ≼ ∪ 𝐴 ) )
21 id ⊢ ( ( card ‘ 𝑦 ) = 𝑦 → ( card ‘ 𝑦 ) = 𝑦 )
22 onenon ⊢ ( ( card ‘ 𝑦 ) ∈ On → ( card ‘ 𝑦 ) ∈ dom card )
23 6 22 ax-mp ⊢ ( card ‘ 𝑦 ) ∈ dom card
24 21 23 syl6eqelr ⊢ ( ( card ‘ 𝑦 ) = 𝑦 → 𝑦 ∈ dom card )
25 onenon ⊢ ( ∪ 𝐴 ∈ On → ∪ 𝐴 ∈ dom card )
26 carddom2 ⊢ ( ( 𝑦 ∈ dom card ∧ ∪ 𝐴 ∈ dom card ) → ( ( card ‘ 𝑦 ) ⊆ ( card ‘ ∪ 𝐴 ) ↔ 𝑦 ≼ ∪ 𝐴 ) )
27 24 25 26 syl2an ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( ( card ‘ 𝑦 ) ⊆ ( card ‘ ∪ 𝐴 ) ↔ 𝑦 ≼ ∪ 𝐴 ) )
28 20 27 sylibrd ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 → ( card ‘ 𝑦 ) ⊆ ( card ‘ ∪ 𝐴 ) ) )
29 sseq1 ⊢ ( ( card ‘ 𝑦 ) = 𝑦 → ( ( card ‘ 𝑦 ) ⊆ ( card ‘ ∪ 𝐴 ) ↔ 𝑦 ⊆ ( card ‘ ∪ 𝐴 ) ) )
30 29 adantr ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( ( card ‘ 𝑦 ) ⊆ ( card ‘ ∪ 𝐴 ) ↔ 𝑦 ⊆ ( card ‘ ∪ 𝐴 ) ) )
31 28 30 sylibd ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 → 𝑦 ⊆ ( card ‘ ∪ 𝐴 ) ) )
32 ssel ⊢ ( 𝑦 ⊆ ( card ‘ ∪ 𝐴 ) → ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) )
33 31 32 syl6 ⊢ ( ( ( card ‘ 𝑦 ) = 𝑦 ∧ ∪ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 → ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) )
34 33 ex ⊢ ( ( card ‘ 𝑦 ) = 𝑦 → ( ∪ 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) ) )
35 34 com3r ⊢ ( 𝑦 ∈ 𝐴 → ( ( card ‘ 𝑦 ) = 𝑦 → ( ∪ 𝐴 ∈ On → ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) ) )
36 5 35 syld ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( ∪ 𝐴 ∈ On → ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) ) )
37 36 com4r ⊢ ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( ∪ 𝐴 ∈ On → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) ) )
38 37 imp ⊢ ( ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( ∪ 𝐴 ∈ On → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) )
39 38 exlimiv ⊢ ( ∃ 𝑦 ( ( card ‘ ∪ 𝐴 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( ∪ 𝐴 ∈ On → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) )
40 16 39 sylbi ⊢ ( ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( ∪ 𝐴 ∈ On → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) )
41 40 com13 ⊢ ( ∪ 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) ) )
42 41 imp ⊢ ( ( ∪ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ( ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) )
43 11 42 sylancom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ( ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 → ( card ‘ ∪ 𝐴 ) ∈ ( card ‘ ∪ 𝐴 ) ) )
44 15 43 mtoi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ¬ ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 )
45 14 onordi ⊢ Ord ( card ‘ ∪ 𝐴 )
46 eloni ⊢ ( ∪ 𝐴 ∈ On → Ord ∪ 𝐴 )
47 11 46 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → Ord ∪ 𝐴 )
48 ordtri4 ⊢ ( ( Ord ( card ‘ ∪ 𝐴 ) ∧ Ord ∪ 𝐴 ) → ( ( card ‘ ∪ 𝐴 ) = ∪ 𝐴 ↔ ( ( card ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 ∧ ¬ ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 ) ) )
49 45 47 48 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ( ( card ‘ ∪ 𝐴 ) = ∪ 𝐴 ↔ ( ( card ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 ∧ ¬ ( card ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 ) ) )
50 13 44 49 mpbir2and ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 ) → ( card ‘ ∪ 𝐴 ) = ∪ 𝐴 )
51 50 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝑥 ) = 𝑥 → ( card ‘ ∪ 𝐴 ) = ∪ 𝐴 ) )