Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  carduni Structured version   Visualization version   GIF version

Theorem carduni 8792
 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.)
Assertion
Ref Expression
carduni (𝐴𝑉 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (card‘ 𝐴) = 𝐴))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem carduni
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6178 . . . . . . . . . 10 (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦))
2 id 22 . . . . . . . . . 10 (𝑥 = 𝑦𝑥 = 𝑦)
31, 2eqeq12d 2635 . . . . . . . . 9 (𝑥 = 𝑦 → ((card‘𝑥) = 𝑥 ↔ (card‘𝑦) = 𝑦))
43rspcv 3300 . . . . . . . 8 (𝑦𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (card‘𝑦) = 𝑦))
5 cardon 8755 . . . . . . . . 9 (card‘𝑦) ∈ On
6 eleq1 2687 . . . . . . . . 9 ((card‘𝑦) = 𝑦 → ((card‘𝑦) ∈ On ↔ 𝑦 ∈ On))
75, 6mpbii 223 . . . . . . . 8 ((card‘𝑦) = 𝑦𝑦 ∈ On)
84, 7syl6com 37 . . . . . . 7 (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (𝑦𝐴𝑦 ∈ On))
98ssrdv 3601 . . . . . 6 (∀𝑥𝐴 (card‘𝑥) = 𝑥𝐴 ⊆ On)
10 ssonuni 6971 . . . . . 6 (𝐴𝑉 → (𝐴 ⊆ On → 𝐴 ∈ On))
119, 10syl5 34 . . . . 5 (𝐴𝑉 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 𝐴 ∈ On))
1211imp 445 . . . 4 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → 𝐴 ∈ On)
13 cardonle 8768 . . . 4 ( 𝐴 ∈ On → (card‘ 𝐴) ⊆ 𝐴)
1412, 13syl 17 . . 3 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → (card‘ 𝐴) ⊆ 𝐴)
15 cardon 8755 . . . . 5 (card‘ 𝐴) ∈ On
1615onirri 5822 . . . 4 ¬ (card‘ 𝐴) ∈ (card‘ 𝐴)
17 eluni 4430 . . . . . . . 8 ((card‘ 𝐴) ∈ 𝐴 ↔ ∃𝑦((card‘ 𝐴) ∈ 𝑦𝑦𝐴))
18 elssuni 4458 . . . . . . . . . . . . . . . . . 18 (𝑦𝐴𝑦 𝐴)
19 ssdomg 7986 . . . . . . . . . . . . . . . . . . 19 ( 𝐴 ∈ On → (𝑦 𝐴𝑦 𝐴))
2019adantl 482 . . . . . . . . . . . . . . . . . 18 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦 𝐴𝑦 𝐴))
2118, 20syl5 34 . . . . . . . . . . . . . . . . 17 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴𝑦 𝐴))
22 id 22 . . . . . . . . . . . . . . . . . . 19 ((card‘𝑦) = 𝑦 → (card‘𝑦) = 𝑦)
23 onenon 8760 . . . . . . . . . . . . . . . . . . . 20 ((card‘𝑦) ∈ On → (card‘𝑦) ∈ dom card)
245, 23ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (card‘𝑦) ∈ dom card
2522, 24syl6eqelr 2708 . . . . . . . . . . . . . . . . . 18 ((card‘𝑦) = 𝑦𝑦 ∈ dom card)
26 onenon 8760 . . . . . . . . . . . . . . . . . 18 ( 𝐴 ∈ On → 𝐴 ∈ dom card)
27 carddom2 8788 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ dom card ∧ 𝐴 ∈ dom card) → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 𝐴))
2825, 26, 27syl2an 494 . . . . . . . . . . . . . . . . 17 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 𝐴))
2921, 28sylibrd 249 . . . . . . . . . . . . . . . 16 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴 → (card‘𝑦) ⊆ (card‘ 𝐴)))
30 sseq1 3618 . . . . . . . . . . . . . . . . 17 ((card‘𝑦) = 𝑦 → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 ⊆ (card‘ 𝐴)))
3130adantr 481 . . . . . . . . . . . . . . . 16 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 ⊆ (card‘ 𝐴)))
3229, 31sylibd 229 . . . . . . . . . . . . . . 15 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴𝑦 ⊆ (card‘ 𝐴)))
33 ssel 3589 . . . . . . . . . . . . . . 15 (𝑦 ⊆ (card‘ 𝐴) → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))
3432, 33syl6 35 . . . . . . . . . . . . . 14 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴 → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴))))
3534ex 450 . . . . . . . . . . . . 13 ((card‘𝑦) = 𝑦 → ( 𝐴 ∈ On → (𝑦𝐴 → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
3635com3r 87 . . . . . . . . . . . 12 (𝑦𝐴 → ((card‘𝑦) = 𝑦 → ( 𝐴 ∈ On → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
374, 36syld 47 . . . . . . . . . . 11 (𝑦𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
3837com4r 94 . . . . . . . . . 10 ((card‘ 𝐴) ∈ 𝑦 → (𝑦𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
3938imp 445 . . . . . . . . 9 (((card‘ 𝐴) ∈ 𝑦𝑦𝐴) → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4039exlimiv 1856 . . . . . . . 8 (∃𝑦((card‘ 𝐴) ∈ 𝑦𝑦𝐴) → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4117, 40sylbi 207 . . . . . . 7 ((card‘ 𝐴) ∈ 𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4241com13 88 . . . . . 6 ( 𝐴 ∈ On → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ((card‘ 𝐴) ∈ 𝐴 → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4342imp 445 . . . . 5 (( 𝐴 ∈ On ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ((card‘ 𝐴) ∈ 𝐴 → (card‘ 𝐴) ∈ (card‘ 𝐴)))
4412, 43sylancom 700 . . . 4 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ((card‘ 𝐴) ∈ 𝐴 → (card‘ 𝐴) ∈ (card‘ 𝐴)))
4516, 44mtoi 190 . . 3 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ¬ (card‘ 𝐴) ∈ 𝐴)
4615onordi 5820 . . . 4 Ord (card‘ 𝐴)
47 eloni 5721 . . . . 5 ( 𝐴 ∈ On → Ord 𝐴)
4812, 47syl 17 . . . 4 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → Ord 𝐴)
49 ordtri4 5749 . . . 4 ((Ord (card‘ 𝐴) ∧ Ord 𝐴) → ((card‘ 𝐴) = 𝐴 ↔ ((card‘ 𝐴) ⊆ 𝐴 ∧ ¬ (card‘ 𝐴) ∈ 𝐴)))
5046, 48, 49sylancr 694 . . 3 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ((card‘ 𝐴) = 𝐴 ↔ ((card‘ 𝐴) ⊆ 𝐴 ∧ ¬ (card‘ 𝐴) ∈ 𝐴)))
5114, 45, 50mpbir2and 956 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → (card‘ 𝐴) = 𝐴)
5251ex 450 1 (𝐴𝑉 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (card‘ 𝐴) = 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1481  ∃wex 1702   ∈ wcel 1988  ∀wral 2909   ⊆ wss 3567  ∪ cuni 4427   class class class wbr 4644  dom cdm 5104  Ord word 5710  Oncon0 5711  ‘cfv 5876   ≼ cdom 7938  cardccrd 8746 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-ord 5714  df-on 5715  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-card 8750 This theorem is referenced by:  cardiun  8793  carduniima  8904
 Copyright terms: Public domain W3C validator