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

Theorem canthwe 9675
Description: The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 8269. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.)
Hypothesis
Ref Expression
canthwe.1 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
Assertion
Ref Expression
canthwe (𝐴𝑉𝐴𝑂)
Distinct variable groups:   𝑥,𝑟,𝑂   𝑉,𝑟,𝑥   𝐴,𝑟,𝑥

Proof of Theorem canthwe
Dummy variables 𝑢 𝑦 𝑓 𝑣 𝑤 𝑎 𝑠 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1130 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥𝐴)
2 selpw 4304 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
31, 2sylibr 224 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
4 simp2 1131 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝑥 × 𝑥))
5 xpss12 5264 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐴) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
61, 1, 5syl2anc 573 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
74, 6sstrd 3762 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝐴 × 𝐴))
8 selpw 4304 . . . . . . . 8 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
97, 8sylibr 224 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
103, 9jca 501 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴)))
1110ssopab2i 5136 . . . . 5 {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
12 canthwe.1 . . . . 5 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
13 df-xp 5255 . . . . 5 (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
1411, 12, 133sstr4i 3793 . . . 4 𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
15 pwexg 4980 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
16 sqxpexg 7110 . . . . . 6 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
17 pwexg 4980 . . . . . 6 ((𝐴 × 𝐴) ∈ V → 𝒫 (𝐴 × 𝐴) ∈ V)
1816, 17syl 17 . . . . 5 (𝐴𝑉 → 𝒫 (𝐴 × 𝐴) ∈ V)
19 xpexg 7107 . . . . 5 ((𝒫 𝐴 ∈ V ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
2015, 18, 19syl2anc 573 . . . 4 (𝐴𝑉 → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
21 ssexg 4938 . . . 4 ((𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V) → 𝑂 ∈ V)
2214, 20, 21sylancr 575 . . 3 (𝐴𝑉𝑂 ∈ V)
23 simpr 471 . . . . . . . 8 ((𝐴𝑉𝑢𝐴) → 𝑢𝐴)
2423snssd 4475 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → {𝑢} ⊆ 𝐴)
25 0ss 4116 . . . . . . . 8 ∅ ⊆ ({𝑢} × {𝑢})
2625a1i 11 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ ⊆ ({𝑢} × {𝑢}))
27 rel0 5382 . . . . . . . 8 Rel ∅
28 br0 4835 . . . . . . . . 9 ¬ 𝑢𝑢
29 wesn 5330 . . . . . . . . 9 (Rel ∅ → (∅ We {𝑢} ↔ ¬ 𝑢𝑢))
3028, 29mpbiri 248 . . . . . . . 8 (Rel ∅ → ∅ We {𝑢})
3127, 30mp1i 13 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ We {𝑢})
32 snex 5036 . . . . . . . 8 {𝑢} ∈ V
33 0ex 4924 . . . . . . . 8 ∅ ∈ V
34 simpl 468 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑥 = {𝑢})
3534sseq1d 3781 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥𝐴 ↔ {𝑢} ⊆ 𝐴))
36 simpr 471 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑟 = ∅)
3734sqxpeqd 5281 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥 × 𝑥) = ({𝑢} × {𝑢}))
3836, 37sseq12d 3783 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ∅ ⊆ ({𝑢} × {𝑢})))
39 weeq2 5238 . . . . . . . . . 10 (𝑥 = {𝑢} → (𝑟 We 𝑥𝑟 We {𝑢}))
40 weeq1 5237 . . . . . . . . . 10 (𝑟 = ∅ → (𝑟 We {𝑢} ↔ ∅ We {𝑢}))
4139, 40sylan9bb 499 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 We 𝑥 ↔ ∅ We {𝑢}))
4235, 38, 413anbi123d 1547 . . . . . . . 8 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢})))
4332, 33, 42opelopaba 5124 . . . . . . 7 (⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢}))
4424, 26, 31, 43syl3anbrc 1428 . . . . . 6 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
4544, 12syl6eleqr 2861 . . . . 5 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ 𝑂)
4645ex 397 . . . 4 (𝐴𝑉 → (𝑢𝐴 → ⟨{𝑢}, ∅⟩ ∈ 𝑂))
47 eqid 2771 . . . . . . 7 ∅ = ∅
48 snex 5036 . . . . . . . 8 {𝑣} ∈ V
4948, 33opth2 5076 . . . . . . 7 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ ({𝑢} = {𝑣} ∧ ∅ = ∅))
5047, 49mpbiran2 689 . . . . . 6 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ {𝑢} = {𝑣})
51 vex 3354 . . . . . . 7 𝑢 ∈ V
52 sneqbg 4506 . . . . . . 7 (𝑢 ∈ V → ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣))
5351, 52ax-mp 5 . . . . . 6 ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣)
5450, 53bitri 264 . . . . 5 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)
55542a1i 12 . . . 4 (𝐴𝑉 → ((𝑢𝐴𝑣𝐴) → (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)))
5646, 55dom2d 8150 . . 3 (𝐴𝑉 → (𝑂 ∈ V → 𝐴𝑂))
5722, 56mpd 15 . 2 (𝐴𝑉𝐴𝑂)
58 eqid 2771 . . . . . . 7 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
5958fpwwe2cbv 9654 . . . . . 6 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑤](𝑤𝑓(𝑟 ∩ (𝑤 × 𝑤))) = 𝑦))}
60 eqid 2771 . . . . . 6 dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
61 eqid 2771 . . . . . 6 (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))}) = (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))})
6212, 59, 60, 61canthwelem 9674 . . . . 5 (𝐴𝑉 → ¬ 𝑓:𝑂1-1𝐴)
63 f1of1 6277 . . . . 5 (𝑓:𝑂1-1-onto𝐴𝑓:𝑂1-1𝐴)
6462, 63nsyl 137 . . . 4 (𝐴𝑉 → ¬ 𝑓:𝑂1-1-onto𝐴)
6564nexdv 2016 . . 3 (𝐴𝑉 → ¬ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
66 ensym 8158 . . . 4 (𝐴𝑂𝑂𝐴)
67 bren 8118 . . . 4 (𝑂𝐴 ↔ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6866, 67sylib 208 . . 3 (𝐴𝑂 → ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6965, 68nsyl 137 . 2 (𝐴𝑉 → ¬ 𝐴𝑂)
70 brsdom 8132 . 2 (𝐴𝑂 ↔ (𝐴𝑂 ∧ ¬ 𝐴𝑂))
7157, 69, 70sylanbrc 572 1 (𝐴𝑉𝐴𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wral 3061  Vcvv 3351  [wsbc 3587  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316  cop 4322   cuni 4574   class class class wbr 4786  {copab 4846   We wwe 5207   × cxp 5247  ccnv 5248  dom cdm 5249  cima 5252  Rel wrel 5254  1-1wf1 6028  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  cen 8106  cdom 8107  csdm 8108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-wrecs 7559  df-recs 7621  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-oi 8571
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator