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

Theorem tskwe 9945
Description: A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
tskwe ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem tskwe
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwexg 5377 . . . 4 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
2 rabexg 5332 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ∈ V)
3 incom 4202 . . . . 5 ({𝑥 ∈ 𝒫 𝐴𝑥𝐴} ∩ On) = (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
4 inex1g 5320 . . . . 5 ({𝑥 ∈ 𝒫 𝐴𝑥𝐴} ∈ V → ({𝑥 ∈ 𝒫 𝐴𝑥𝐴} ∩ On) ∈ V)
53, 4eqeltrrid 2839 . . . 4 ({𝑥 ∈ 𝒫 𝐴𝑥𝐴} ∈ V → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ V)
6 inss1 4229 . . . . . . . . . . 11 (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ On
76sseli 3979 . . . . . . . . . 10 (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → 𝑧 ∈ On)
8 onelon 6390 . . . . . . . . . . 11 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦 ∈ On)
98ancoms 460 . . . . . . . . . 10 ((𝑦𝑧𝑧 ∈ On) → 𝑦 ∈ On)
107, 9sylan2 594 . . . . . . . . 9 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦 ∈ On)
11 onelss 6407 . . . . . . . . . . . . . 14 (𝑧 ∈ On → (𝑦𝑧𝑦𝑧))
1211impcom 409 . . . . . . . . . . . . 13 ((𝑦𝑧𝑧 ∈ On) → 𝑦𝑧)
137, 12sylan2 594 . . . . . . . . . . . 12 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦𝑧)
14 inss2 4230 . . . . . . . . . . . . . . . . 17 (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}
1514sseli 3979 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
16 breq1 5152 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1716elrab 3684 . . . . . . . . . . . . . . . 16 (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ↔ (𝑧 ∈ 𝒫 𝐴𝑧𝐴))
1815, 17sylib 217 . . . . . . . . . . . . . . 15 (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → (𝑧 ∈ 𝒫 𝐴𝑧𝐴))
1918simpld 496 . . . . . . . . . . . . . 14 (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → 𝑧 ∈ 𝒫 𝐴)
2019elpwid 4612 . . . . . . . . . . . . 13 (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → 𝑧𝐴)
2120adantl 483 . . . . . . . . . . . 12 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑧𝐴)
2213, 21sstrd 3993 . . . . . . . . . . 11 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦𝐴)
23 velpw 4608 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
2422, 23sylibr 233 . . . . . . . . . 10 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦 ∈ 𝒫 𝐴)
25 vex 3479 . . . . . . . . . . . 12 𝑧 ∈ V
26 ssdomg 8996 . . . . . . . . . . . 12 (𝑧 ∈ V → (𝑦𝑧𝑦𝑧))
2725, 13, 26mpsyl 68 . . . . . . . . . . 11 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦𝑧)
2818simprd 497 . . . . . . . . . . . 12 (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → 𝑧𝐴)
2928adantl 483 . . . . . . . . . . 11 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑧𝐴)
30 domsdomtr 9112 . . . . . . . . . . 11 ((𝑦𝑧𝑧𝐴) → 𝑦𝐴)
3127, 29, 30syl2anc 585 . . . . . . . . . 10 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦𝐴)
32 breq1 5152 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3332elrab 3684 . . . . . . . . . 10 (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ↔ (𝑦 ∈ 𝒫 𝐴𝑦𝐴))
3424, 31, 33sylanbrc 584 . . . . . . . . 9 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
3510, 34elind 4195 . . . . . . . 8 ((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}))
3635gen2 1799 . . . . . . 7 𝑦𝑧((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}))
37 dftr2 5268 . . . . . . 7 (Tr (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ↔ ∀𝑦𝑧((𝑦𝑧𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})) → 𝑦 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})))
3836, 37mpbir 230 . . . . . 6 Tr (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
39 ordon 7764 . . . . . 6 Ord On
40 trssord 6382 . . . . . 6 ((Tr (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ On ∧ Ord On) → Ord (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}))
4138, 6, 39, 40mp3an 1462 . . . . 5 Ord (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
42 elong 6373 . . . . 5 ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ V → ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ On ↔ Ord (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})))
4341, 42mpbiri 258 . . . 4 ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ V → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ On)
441, 2, 5, 434syl 19 . . 3 (𝐴𝑉 → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ On)
4544adantr 482 . 2 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ On)
46 simpr 486 . . . . 5 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴)
4714, 46sstrid 3994 . . . 4 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ 𝐴)
48 ssdomg 8996 . . . . 5 (𝐴𝑉 → ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ 𝐴 → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≼ 𝐴))
4948adantr 482 . . . 4 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ 𝐴 → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≼ 𝐴))
5047, 49mpd 15 . . 3 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≼ 𝐴)
51 ordirr 6383 . . . . 5 (Ord (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}))
5241, 51mp1i 13 . . . 4 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}))
53443ad2ant1 1134 . . . . . 6 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ On)
54 elpw2g 5345 . . . . . . . . . 10 (𝐴𝑉 → ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ 𝒫 𝐴 ↔ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ 𝐴))
5554adantr 482 . . . . . . . . 9 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ 𝒫 𝐴 ↔ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ⊆ 𝐴))
5647, 55mpbird 257 . . . . . . . 8 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ 𝒫 𝐴)
57563adant3 1133 . . . . . . 7 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ 𝒫 𝐴)
58 simp3 1139 . . . . . . 7 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴)
59 nfcv 2904 . . . . . . . . 9 𝑥On
60 nfrab1 3452 . . . . . . . . 9 𝑥{𝑥 ∈ 𝒫 𝐴𝑥𝐴}
6159, 60nfin 4217 . . . . . . . 8 𝑥(On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
62 nfcv 2904 . . . . . . . 8 𝑥𝒫 𝐴
63 nfcv 2904 . . . . . . . . 9 𝑥
64 nfcv 2904 . . . . . . . . 9 𝑥𝐴
6561, 63, 64nfbr 5196 . . . . . . . 8 𝑥(On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴
66 breq1 5152 . . . . . . . 8 (𝑥 = (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) → (𝑥𝐴 ↔ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴))
6761, 62, 65, 66elrabf 3680 . . . . . . 7 ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ↔ ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ 𝒫 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴))
6857, 58, 67sylanbrc 584 . . . . . 6 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})
6953, 68elind 4195 . . . . 5 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}))
70693expia 1122 . . . 4 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴 → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴})))
7152, 70mtod 197 . . 3 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴)
72 bren2 8979 . . 3 ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≈ 𝐴 ↔ ((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≼ 𝐴 ∧ ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≺ 𝐴))
7350, 71, 72sylanbrc 584 . 2 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≈ 𝐴)
74 isnumi 9941 . 2 (((On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ∈ On ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴𝑥𝐴}) ≈ 𝐴) → 𝐴 ∈ dom card)
7545, 73, 74syl2anc 585 1 ((𝐴𝑉 ∧ {𝑥 ∈ 𝒫 𝐴𝑥𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088  wal 1540  wcel 2107  {crab 3433  Vcvv 3475  cin 3948  wss 3949  𝒫 cpw 4603   class class class wbr 5149  Tr wtr 5266  dom cdm 5677  Ord word 6364  Oncon0 6365  cen 8936  cdom 8937  csdm 8938  cardccrd 9930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-card 9934
This theorem is referenced by:  tskwe2  10768  grothac  10825
  Copyright terms: Public domain W3C validator