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

Theorem carduni 9448
 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 ssonuni 7505 . . . . 5 (𝐴𝑉 → (𝐴 ⊆ On → 𝐴 ∈ On))
2 fveq2 6662 . . . . . . . . 9 (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦))
3 id 22 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
42, 3eqeq12d 2774 . . . . . . . 8 (𝑥 = 𝑦 → ((card‘𝑥) = 𝑥 ↔ (card‘𝑦) = 𝑦))
54rspcv 3538 . . . . . . 7 (𝑦𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (card‘𝑦) = 𝑦))
6 cardon 9411 . . . . . . . 8 (card‘𝑦) ∈ On
7 eleq1 2839 . . . . . . . 8 ((card‘𝑦) = 𝑦 → ((card‘𝑦) ∈ On ↔ 𝑦 ∈ On))
86, 7mpbii 236 . . . . . . 7 ((card‘𝑦) = 𝑦𝑦 ∈ On)
95, 8syl6com 37 . . . . . 6 (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (𝑦𝐴𝑦 ∈ On))
109ssrdv 3900 . . . . 5 (∀𝑥𝐴 (card‘𝑥) = 𝑥𝐴 ⊆ On)
111, 10impel 509 . . . 4 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → 𝐴 ∈ On)
12 cardonle 9424 . . . 4 ( 𝐴 ∈ On → (card‘ 𝐴) ⊆ 𝐴)
1311, 12syl 17 . . 3 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → (card‘ 𝐴) ⊆ 𝐴)
14 cardon 9411 . . . . 5 (card‘ 𝐴) ∈ On
1514onirri 6280 . . . 4 ¬ (card‘ 𝐴) ∈ (card‘ 𝐴)
16 eluni 4804 . . . . . . . 8 ((card‘ 𝐴) ∈ 𝐴 ↔ ∃𝑦((card‘ 𝐴) ∈ 𝑦𝑦𝐴))
17 elssuni 4833 . . . . . . . . . . . . . . . . . 18 (𝑦𝐴𝑦 𝐴)
18 ssdomg 8578 . . . . . . . . . . . . . . . . . . 19 ( 𝐴 ∈ On → (𝑦 𝐴𝑦 𝐴))
1918adantl 485 . . . . . . . . . . . . . . . . . 18 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦 𝐴𝑦 𝐴))
2017, 19syl5 34 . . . . . . . . . . . . . . . . 17 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴𝑦 𝐴))
21 id 22 . . . . . . . . . . . . . . . . . . 19 ((card‘𝑦) = 𝑦 → (card‘𝑦) = 𝑦)
22 onenon 9416 . . . . . . . . . . . . . . . . . . . 20 ((card‘𝑦) ∈ On → (card‘𝑦) ∈ dom card)
236, 22ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (card‘𝑦) ∈ dom card
2421, 23eqeltrrdi 2861 . . . . . . . . . . . . . . . . . 18 ((card‘𝑦) = 𝑦𝑦 ∈ dom card)
25 onenon 9416 . . . . . . . . . . . . . . . . . 18 ( 𝐴 ∈ On → 𝐴 ∈ dom card)
26 carddom2 9444 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ dom card ∧ 𝐴 ∈ dom card) → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 𝐴))
2724, 25, 26syl2an 598 . . . . . . . . . . . . . . . . 17 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 𝐴))
2820, 27sylibrd 262 . . . . . . . . . . . . . . . 16 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴 → (card‘𝑦) ⊆ (card‘ 𝐴)))
29 sseq1 3919 . . . . . . . . . . . . . . . . 17 ((card‘𝑦) = 𝑦 → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 ⊆ (card‘ 𝐴)))
3029adantr 484 . . . . . . . . . . . . . . . 16 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → ((card‘𝑦) ⊆ (card‘ 𝐴) ↔ 𝑦 ⊆ (card‘ 𝐴)))
3128, 30sylibd 242 . . . . . . . . . . . . . . 15 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴𝑦 ⊆ (card‘ 𝐴)))
32 ssel 3887 . . . . . . . . . . . . . . 15 (𝑦 ⊆ (card‘ 𝐴) → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))
3331, 32syl6 35 . . . . . . . . . . . . . 14 (((card‘𝑦) = 𝑦 𝐴 ∈ On) → (𝑦𝐴 → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴))))
3433ex 416 . . . . . . . . . . . . 13 ((card‘𝑦) = 𝑦 → ( 𝐴 ∈ On → (𝑦𝐴 → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
3534com3r 87 . . . . . . . . . . . 12 (𝑦𝐴 → ((card‘𝑦) = 𝑦 → ( 𝐴 ∈ On → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
365, 35syld 47 . . . . . . . . . . 11 (𝑦𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → ((card‘ 𝐴) ∈ 𝑦 → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
3736com4r 94 . . . . . . . . . 10 ((card‘ 𝐴) ∈ 𝑦 → (𝑦𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴)))))
3837imp 410 . . . . . . . . 9 (((card‘ 𝐴) ∈ 𝑦𝑦𝐴) → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴))))
3938exlimiv 1931 . . . . . . . 8 (∃𝑦((card‘ 𝐴) ∈ 𝑦𝑦𝐴) → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4016, 39sylbi 220 . . . . . . 7 ((card‘ 𝐴) ∈ 𝐴 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ( 𝐴 ∈ On → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4140com13 88 . . . . . 6 ( 𝐴 ∈ On → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → ((card‘ 𝐴) ∈ 𝐴 → (card‘ 𝐴) ∈ (card‘ 𝐴))))
4241imp 410 . . . . 5 (( 𝐴 ∈ On ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ((card‘ 𝐴) ∈ 𝐴 → (card‘ 𝐴) ∈ (card‘ 𝐴)))
4311, 42sylancom 591 . . . 4 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ((card‘ 𝐴) ∈ 𝐴 → (card‘ 𝐴) ∈ (card‘ 𝐴)))
4415, 43mtoi 202 . . 3 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ¬ (card‘ 𝐴) ∈ 𝐴)
4514onordi 6278 . . . 4 Ord (card‘ 𝐴)
46 eloni 6183 . . . . 5 ( 𝐴 ∈ On → Ord 𝐴)
4711, 46syl 17 . . . 4 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → Ord 𝐴)
48 ordtri4 6210 . . . 4 ((Ord (card‘ 𝐴) ∧ Ord 𝐴) → ((card‘ 𝐴) = 𝐴 ↔ ((card‘ 𝐴) ⊆ 𝐴 ∧ ¬ (card‘ 𝐴) ∈ 𝐴)))
4945, 47, 48sylancr 590 . . 3 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → ((card‘ 𝐴) = 𝐴 ↔ ((card‘ 𝐴) ⊆ 𝐴 ∧ ¬ (card‘ 𝐴) ∈ 𝐴)))
5013, 44, 49mpbir2and 712 . 2 ((𝐴𝑉 ∧ ∀𝑥𝐴 (card‘𝑥) = 𝑥) → (card‘ 𝐴) = 𝐴)
5150ex 416 1 (𝐴𝑉 → (∀𝑥𝐴 (card‘𝑥) = 𝑥 → (card‘ 𝐴) = 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070   ⊆ wss 3860  ∪ cuni 4801   class class class wbr 5035  dom cdm 5527  Ord word 6172  Oncon0 6173  ‘cfv 6339   ≼ cdom 8530  cardccrd 9402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-ord 6176  df-on 6177  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-card 9406 This theorem is referenced by:  cardiun  9449  carduniima  9561
 Copyright terms: Public domain W3C validator