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

Theorem canthwe 10668
Description: The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 9148. 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 1134 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥𝐴)
2 velpw 4603 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
31, 2sylibr 233 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
4 simp2 1135 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝑥 × 𝑥))
5 xpss12 5687 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐴) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
61, 1, 5syl2anc 583 . . . . . . . . 9 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
74, 6sstrd 3988 . . . . . . . 8 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝐴 × 𝐴))
8 velpw 4603 . . . . . . . 8 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
97, 8sylibr 233 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
103, 9jca 511 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴)))
1110ssopab2i 5546 . . . . 5 {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
12 canthwe.1 . . . . 5 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}
13 df-xp 5678 . . . . 5 (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ∈ 𝒫 𝐴𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
1411, 12, 133sstr4i 4021 . . . 4 𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
15 pwexg 5372 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
16 sqxpexg 7751 . . . . . 6 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
1716pwexd 5373 . . . . 5 (𝐴𝑉 → 𝒫 (𝐴 × 𝐴) ∈ V)
1815, 17xpexd 7747 . . . 4 (𝐴𝑉 → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V)
19 ssexg 5317 . . . 4 ((𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V) → 𝑂 ∈ V)
2014, 18, 19sylancr 586 . . 3 (𝐴𝑉𝑂 ∈ V)
21 simpr 484 . . . . . . . 8 ((𝐴𝑉𝑢𝐴) → 𝑢𝐴)
2221snssd 4808 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → {𝑢} ⊆ 𝐴)
23 0ss 4392 . . . . . . . 8 ∅ ⊆ ({𝑢} × {𝑢})
2423a1i 11 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ ⊆ ({𝑢} × {𝑢}))
25 rel0 5795 . . . . . . . 8 Rel ∅
26 br0 5191 . . . . . . . . 9 ¬ 𝑢𝑢
27 wesn 5760 . . . . . . . . 9 (Rel ∅ → (∅ We {𝑢} ↔ ¬ 𝑢𝑢))
2826, 27mpbiri 258 . . . . . . . 8 (Rel ∅ → ∅ We {𝑢})
2925, 28mp1i 13 . . . . . . 7 ((𝐴𝑉𝑢𝐴) → ∅ We {𝑢})
30 vsnex 5425 . . . . . . . 8 {𝑢} ∈ V
31 0ex 5301 . . . . . . . 8 ∅ ∈ V
32 simpl 482 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑥 = {𝑢})
3332sseq1d 4009 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥𝐴 ↔ {𝑢} ⊆ 𝐴))
34 simpr 484 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑟 = ∅)
3532sqxpeqd 5704 . . . . . . . . . 10 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥 × 𝑥) = ({𝑢} × {𝑢}))
3634, 35sseq12d 4011 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ∅ ⊆ ({𝑢} × {𝑢})))
37 weeq2 5661 . . . . . . . . . 10 (𝑥 = {𝑢} → (𝑟 We 𝑥𝑟 We {𝑢}))
38 weeq1 5660 . . . . . . . . . 10 (𝑟 = ∅ → (𝑟 We {𝑢} ↔ ∅ We {𝑢}))
3937, 38sylan9bb 509 . . . . . . . . 9 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 We 𝑥 ↔ ∅ We {𝑢}))
4033, 36, 393anbi123d 1433 . . . . . . . 8 ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢})))
4130, 31, 40opelopaba 5532 . . . . . . 7 (⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢}))
4222, 24, 29, 41syl3anbrc 1341 . . . . . 6 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ {⟨𝑥, 𝑟⟩ ∣ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)})
4342, 12eleqtrrdi 2840 . . . . 5 ((𝐴𝑉𝑢𝐴) → ⟨{𝑢}, ∅⟩ ∈ 𝑂)
4443ex 412 . . . 4 (𝐴𝑉 → (𝑢𝐴 → ⟨{𝑢}, ∅⟩ ∈ 𝑂))
45 eqid 2728 . . . . . . 7 ∅ = ∅
46 vsnex 5425 . . . . . . . 8 {𝑣} ∈ V
4746, 31opth2 5476 . . . . . . 7 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ ({𝑢} = {𝑣} ∧ ∅ = ∅))
4845, 47mpbiran2 709 . . . . . 6 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ {𝑢} = {𝑣})
49 sneqbg 4840 . . . . . . 7 (𝑢 ∈ V → ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣))
5049elv 3476 . . . . . 6 ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣)
5148, 50bitri 275 . . . . 5 (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)
52512a1i 12 . . . 4 (𝐴𝑉 → ((𝑢𝐴𝑣𝐴) → (⟨{𝑢}, ∅⟩ = ⟨{𝑣}, ∅⟩ ↔ 𝑢 = 𝑣)))
5344, 52dom2d 9007 . . 3 (𝐴𝑉 → (𝑂 ∈ V → 𝐴𝑂))
5420, 53mpd 15 . 2 (𝐴𝑉𝐴𝑂)
55 eqid 2728 . . . . . . 7 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
5655fpwwe2cbv 10647 . . . . . 6 {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑤](𝑤𝑓(𝑟 ∩ (𝑤 × 𝑤))) = 𝑦))}
57 eqid 2728 . . . . . 6 dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
58 eqid 2728 . . . . . 6 (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))}) = (({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {( dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘ dom {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))})
5912, 56, 57, 58canthwelem 10667 . . . . 5 (𝐴𝑉 → ¬ 𝑓:𝑂1-1𝐴)
60 f1of1 6832 . . . . 5 (𝑓:𝑂1-1-onto𝐴𝑓:𝑂1-1𝐴)
6159, 60nsyl 140 . . . 4 (𝐴𝑉 → ¬ 𝑓:𝑂1-1-onto𝐴)
6261nexdv 1932 . . 3 (𝐴𝑉 → ¬ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
63 ensym 9017 . . . 4 (𝐴𝑂𝑂𝐴)
64 bren 8967 . . . 4 (𝑂𝐴 ↔ ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6563, 64sylib 217 . . 3 (𝐴𝑂 → ∃𝑓 𝑓:𝑂1-1-onto𝐴)
6662, 65nsyl 140 . 2 (𝐴𝑉 → ¬ 𝐴𝑂)
67 brsdom 8989 . 2 (𝐴𝑂 ↔ (𝐴𝑂 ∧ ¬ 𝐴𝑂))
6854, 66, 67sylanbrc 582 1 (𝐴𝑉𝐴𝑂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wex 1774  wcel 2099  wral 3057  Vcvv 3470  [wsbc 3775  cin 3944  wss 3945  c0 4318  𝒫 cpw 4598  {csn 4624  cop 4630   cuni 4903   class class class wbr 5142  {copab 5204   We wwe 5626   × cxp 5670  ccnv 5671  dom cdm 5672  cima 5675  Rel wrel 5677  1-1wf1 6539  1-1-ontowf1o 6541  cfv 6542  (class class class)co 7414  cen 8954  cdom 8955  csdm 8956
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-oi 9527
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator