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 eqeltrrdi ( ( 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 ‘ 𝐴 ) = 𝐴 ) )