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

Theorem canthwe 9330
Description: The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 7976. 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 1053 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥𝐴)
2 selpw 4114 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
31, 2sylibr 222 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
4 simp2 1054 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝑥 × 𝑥))
5 xpss12 5137 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐴) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
61, 1, 5syl2anc 690 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
74, 6sstrd 3577 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝐴 × 𝐴))
8 selpw 4114 . . . . . . . 8 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
97, 8sylibr 222 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
103, 9jca 552 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴)))
1110ssopab2i 4918 . . . . 5 {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
12 canthwe.1 . . . . 5 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
13 df-xp 5034 . . . . 5 (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
1411, 12, 133sstr4i 3606 . . . 4 𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
15 pwexg 4771 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
16 sqxpexg 6839 . . . . . 6 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
17 pwexg 4771 . . . . . 6 ((𝐴 × 𝐴) ∈ V → 𝒫 (𝐴 × 𝐴) ∈ V)
1816, 17syl 17 . . . . 5 (𝐴𝑉 → 𝒫 (𝐴 × 𝐴) ∈ V)
19 xpexg 6836 . . . . 5 ((𝒫 𝐴 ∈ V ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
2015, 18, 19syl2anc 690 . . . 4 (𝐴𝑉 → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
21 ssexg 4727 . . . 4 ((𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V) → 𝑂 ∈ V)
2214, 20, 21sylancr 693 . . 3 (𝐴𝑉𝑂 ∈ V)
23 simpr 475 . . . . . . . 8 ((𝐴𝑉𝑢𝐴) → 𝑢𝐴)
2423snssd 4280 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → {𝑢} ⊆ 𝐴)
25 0ss 3923 . . . . . . . 8 ∅ ⊆ ({𝑢} × {𝑢})
2625a1i 11 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ ⊆ ({𝑢} × {𝑢}))
27 rel0 5155 . . . . . . . 8 Rel ∅
28 br0 4625 . . . . . . . . 9 ¬ 𝑢𝑢
29 wesn 5103 . . . . . . . . 9 (Rel ∅ → (∅ We {𝑢} ↔ ¬ 𝑢𝑢))
3028, 29mpbiri 246 . . . . . . . 8 (Rel ∅ → ∅ We {𝑢})
3127, 30mp1i 13 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ We {𝑢})
32 snex 4830 . . . . . . . 8 {𝑢} ∈ V
33 0ex 4713 . . . . . . . 8 ∅ ∈ V
34 simpl 471 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑥 = {𝑢})
3534sseq1d 3594 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥𝐴 ↔ {𝑢} ⊆ 𝐴))
36 simpr 475 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑟 = ∅)
3734sqxpeqd 5055 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥 × 𝑥) = ({𝑢} × {𝑢}))
3836, 37sseq12d 3596 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ∅ ⊆ ({𝑢} × {𝑢})))
39 weeq2 5017 . . . . . . . . . 10 (𝑥 = {𝑢} → (𝑟 We 𝑥𝑟 We {𝑢}))
40 weeq1 5016 . . . . . . . . . 10 (𝑟 = ∅ → (𝑟 We {𝑢} ↔ ∅ We {𝑢}))
4139, 40sylan9bb 731 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 We 𝑥 ↔ ∅ We {𝑢}))
4235, 38, 413anbi123d 1390 . . . . . . . 8 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢})))
4332, 33, 42opelopaba 4906 . . . . . . 7 (⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢}))
4424, 26, 31, 43syl3anbrc 1238 . . . . . 6 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
4544, 12syl6eleqr 2698 . . . . 5 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ 𝑂)
4645ex 448 . . . 4 (𝐴𝑉 → (𝑢𝐴 → ⟨{𝑢}, ∅⟩ ∈ 𝑂))
47 eqid 2609 . . . . . . 7 ∅ = ∅
48 snex 4830 . . . . . . . 8 {𝑣} ∈ V
4948, 33opth2 4869 . . . . . . 7 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ ({𝑢} = {𝑣} ∧ ∅ = ∅))
5047, 49mpbiran2 955 . . . . . 6 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ {𝑢} = {𝑣})
51 vex 3175 . . . . . . 7 𝑢 ∈ V
52 sneqbg 4309 . . . . . . 7 (𝑢 ∈ V → ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣))
5351, 52ax-mp 5 . . . . . 6 ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣)
5450, 53bitri 262 . . . . 5 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)
55542a1i 12 . . . 4 (𝐴𝑉 → ((𝑢𝐴𝑣𝐴) → (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)))
5646, 55dom2d 7860 . . 3 (𝐴𝑉 → (𝑂 ∈ V → 𝐴𝑂))
5722, 56mpd 15 . 2 (𝐴𝑉𝐴𝑂)
58 eqid 2609 . . . . . . 7 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
5958fpwwe2cbv 9309 . . . . . 6 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑤](𝑤𝑓(𝑟 ∩ (𝑤 × 𝑤))) = 𝑦))}
60 eqid 2609 . . . . . 6 dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
61 eqid 2609 . . . . . 6 (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))}) = (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))})
6212, 59, 60, 61canthwelem 9329 . . . . 5 (𝐴𝑉 → ¬ 𝑓:𝑂1-1𝐴)
63 f1of1 6034 . . . . 5 (𝑓:𝑂1-1-onto𝐴𝑓:𝑂1-1𝐴)
6462, 63nsyl 133 . . . 4 (𝐴𝑉 → ¬ 𝑓:𝑂1-1-onto𝐴)
6564nexdv 1850 . . 3 (𝐴𝑉 → ¬ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
66 ensym 7869 . . . 4 (𝐴𝑂𝑂𝐴)
67 bren 7828 . . . 4 (𝑂𝐴 ↔ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6866, 67sylib 206 . . 3 (𝐴𝑂 → ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6965, 68nsyl 133 . 2 (𝐴𝑉 → ¬ 𝐴𝑂)
70 brsdom 7842 . 2 (𝐴𝑂 ↔ (𝐴𝑂 ∧ ¬ 𝐴𝑂))
7157, 69, 70sylanbrc 694 1 (𝐴𝑉𝐴𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wral 2895  Vcvv 3172  [wsbc 3401  cin 3538  wss 3539  c0 3873  𝒫 cpw 4107  {csn 4124  cop 4130   cuni 4366   class class class wbr 4577  {copab 4636   We wwe 4986   × cxp 5026  ccnv 5027  dom cdm 5028  cima 5031  Rel wrel 5033  1-1wf1 5787  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cen 7816  cdom 7817  csdm 7818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-wrecs 7272  df-recs 7333  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-oi 8276
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator