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

Theorem canthwe 9761
Description: The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 8355. 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 1159 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥𝐴)
2 selpw 4365 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
31, 2sylibr 225 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
4 simp2 1160 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝑥 × 𝑥))
5 xpss12 5333 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐴) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
61, 1, 5syl2anc 575 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
74, 6sstrd 3815 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝐴 × 𝐴))
8 selpw 4365 . . . . . . . 8 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
97, 8sylibr 225 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
103, 9jca 503 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴)))
1110ssopab2i 5205 . . . . 5 {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
12 canthwe.1 . . . . 5 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
13 df-xp 5324 . . . . 5 (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
1411, 12, 133sstr4i 3848 . . . 4 𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
15 pwexg 5055 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
16 sqxpexg 7196 . . . . . 6 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
1716pwexd 5056 . . . . 5 (𝐴𝑉 → 𝒫 (𝐴 × 𝐴) ∈ V)
18 xpexg 7193 . . . . 5 ((𝒫 𝐴 ∈ V ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
1915, 17, 18syl2anc 575 . . . 4 (𝐴𝑉 → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
20 ssexg 5006 . . . 4 ((𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V) → 𝑂 ∈ V)
2114, 19, 20sylancr 577 . . 3 (𝐴𝑉𝑂 ∈ V)
22 simpr 473 . . . . . . . 8 ((𝐴𝑉𝑢𝐴) → 𝑢𝐴)
2322snssd 4537 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → {𝑢} ⊆ 𝐴)
24 0ss 4177 . . . . . . . 8 ∅ ⊆ ({𝑢} × {𝑢})
2524a1i 11 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ ⊆ ({𝑢} × {𝑢}))
26 rel0 5452 . . . . . . . 8 Rel ∅
27 br0 4900 . . . . . . . . 9 ¬ 𝑢𝑢
28 wesn 5399 . . . . . . . . 9 (Rel ∅ → (∅ We {𝑢} ↔ ¬ 𝑢𝑢))
2927, 28mpbiri 249 . . . . . . . 8 (Rel ∅ → ∅ We {𝑢})
3026, 29mp1i 13 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ We {𝑢})
31 snex 5105 . . . . . . . 8 {𝑢} ∈ V
32 0ex 4991 . . . . . . . 8 ∅ ∈ V
33 simpl 470 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑥 = {𝑢})
3433sseq1d 3836 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥𝐴 ↔ {𝑢} ⊆ 𝐴))
35 simpr 473 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑟 = ∅)
3633sqxpeqd 5349 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥 × 𝑥) = ({𝑢} × {𝑢}))
3735, 36sseq12d 3838 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ∅ ⊆ ({𝑢} × {𝑢})))
38 weeq2 5307 . . . . . . . . . 10 (𝑥 = {𝑢} → (𝑟 We 𝑥𝑟 We {𝑢}))
39 weeq1 5306 . . . . . . . . . 10 (𝑟 = ∅ → (𝑟 We {𝑢} ↔ ∅ We {𝑢}))
4038, 39sylan9bb 501 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 We 𝑥 ↔ ∅ We {𝑢}))
4134, 37, 403anbi123d 1553 . . . . . . . 8 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢})))
4231, 32, 41opelopaba 5193 . . . . . . 7 (⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢}))
4323, 25, 30, 42syl3anbrc 1436 . . . . . 6 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
4443, 12syl6eleqr 2903 . . . . 5 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ 𝑂)
4544ex 399 . . . 4 (𝐴𝑉 → (𝑢𝐴 → ⟨{𝑢}, ∅⟩ ∈ 𝑂))
46 eqid 2813 . . . . . . 7 ∅ = ∅
47 snex 5105 . . . . . . . 8 {𝑣} ∈ V
4847, 32opth2 5145 . . . . . . 7 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ ({𝑢} = {𝑣} ∧ ∅ = ∅))
4946, 48mpbiran2 692 . . . . . 6 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ {𝑢} = {𝑣})
50 vex 3401 . . . . . . 7 𝑢 ∈ V
51 sneqbg 4569 . . . . . . 7 (𝑢 ∈ V → ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣))
5250, 51ax-mp 5 . . . . . 6 ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣)
5349, 52bitri 266 . . . . 5 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)
54532a1i 12 . . . 4 (𝐴𝑉 → ((𝑢𝐴𝑣𝐴) → (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)))
5545, 54dom2d 8236 . . 3 (𝐴𝑉 → (𝑂 ∈ V → 𝐴𝑂))
5621, 55mpd 15 . 2 (𝐴𝑉𝐴𝑂)
57 eqid 2813 . . . . . . 7 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
5857fpwwe2cbv 9740 . . . . . 6 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑤](𝑤𝑓(𝑟 ∩ (𝑤 × 𝑤))) = 𝑦))}
59 eqid 2813 . . . . . 6 dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
60 eqid 2813 . . . . . 6 (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))}) = (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))})
6112, 58, 59, 60canthwelem 9760 . . . . 5 (𝐴𝑉 → ¬ 𝑓:𝑂1-1𝐴)
62 f1of1 6355 . . . . 5 (𝑓:𝑂1-1-onto𝐴𝑓:𝑂1-1𝐴)
6361, 62nsyl 137 . . . 4 (𝐴𝑉 → ¬ 𝑓:𝑂1-1-onto𝐴)
6463nexdv 2027 . . 3 (𝐴𝑉 → ¬ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
65 ensym 8244 . . . 4 (𝐴𝑂𝑂𝐴)
66 bren 8204 . . . 4 (𝑂𝐴 ↔ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6765, 66sylib 209 . . 3 (𝐴𝑂 → ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6864, 67nsyl 137 . 2 (𝐴𝑉 → ¬ 𝐴𝑂)
69 brsdom 8218 . 2 (𝐴𝑂 ↔ (𝐴𝑂 ∧ ¬ 𝐴𝑂))
7056, 68, 69sylanbrc 574 1 (𝐴𝑉𝐴𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wral 3103  Vcvv 3398  [wsbc 3640  cin 3775  wss 3776  c0 4123  𝒫 cpw 4358  {csn 4377  cop 4383   cuni 4637   class class class wbr 4851  {copab 4913   We wwe 5276   × cxp 5316  ccnv 5317  dom cdm 5318  cima 5321  Rel wrel 5323  1-1wf1 6101  1-1-ontowf1o 6103  cfv 6104  (class class class)co 6877  cen 8192  cdom 8193  csdm 8194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-wrecs 7645  df-recs 7707  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-oi 8657
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator