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

Theorem canthp1lem1 10596
Description: Lemma for canthp1 10598. (Contributed by Mario Carneiro, 18-May-2015.)
Assertion
Ref Expression
canthp1lem1 (1o𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)

Proof of Theorem canthp1lem1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 1sdom2 9190 . . 3 1o ≺ 2o
2 djuxpdom 10129 . . 3 ((1o𝐴 ∧ 1o ≺ 2o) → (𝐴 ⊔ 2o) ≼ (𝐴 × 2o))
31, 2mpan2 690 . 2 (1o𝐴 → (𝐴 ⊔ 2o) ≼ (𝐴 × 2o))
4 sdom0 9058 . . . . . 6 ¬ 1o ≺ ∅
5 breq2 5113 . . . . . 6 (𝐴 = ∅ → (1o𝐴 ↔ 1o ≺ ∅))
64, 5mtbiri 327 . . . . 5 (𝐴 = ∅ → ¬ 1o𝐴)
76con2i 139 . . . 4 (1o𝐴 → ¬ 𝐴 = ∅)
8 neq0 4309 . . . 4 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
97, 8sylib 217 . . 3 (1o𝐴 → ∃𝑥 𝑥𝐴)
10 relsdom 8896 . . . . . . . . . 10 Rel ≺
1110brrelex2i 5693 . . . . . . . . 9 (1o𝐴𝐴 ∈ V)
1211adantr 482 . . . . . . . 8 ((1o𝐴𝑥𝐴) → 𝐴 ∈ V)
13 enrefg 8930 . . . . . . . 8 (𝐴 ∈ V → 𝐴𝐴)
1412, 13syl 17 . . . . . . 7 ((1o𝐴𝑥𝐴) → 𝐴𝐴)
15 df2o2 8425 . . . . . . . . 9 2o = {∅, {∅}}
16 pwpw0 4777 . . . . . . . . 9 𝒫 {∅} = {∅, {∅}}
1715, 16eqtr4i 2764 . . . . . . . 8 2o = 𝒫 {∅}
18 0ex 5268 . . . . . . . . . 10 ∅ ∈ V
19 vex 3451 . . . . . . . . . 10 𝑥 ∈ V
20 en2sn 8991 . . . . . . . . . 10 ((∅ ∈ V ∧ 𝑥 ∈ V) → {∅} ≈ {𝑥})
2118, 19, 20mp2an 691 . . . . . . . . 9 {∅} ≈ {𝑥}
22 pwen 9100 . . . . . . . . 9 ({∅} ≈ {𝑥} → 𝒫 {∅} ≈ 𝒫 {𝑥})
2321, 22ax-mp 5 . . . . . . . 8 𝒫 {∅} ≈ 𝒫 {𝑥}
2417, 23eqbrtri 5130 . . . . . . 7 2o ≈ 𝒫 {𝑥}
25 xpen 9090 . . . . . . 7 ((𝐴𝐴 ∧ 2o ≈ 𝒫 {𝑥}) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥}))
2614, 24, 25sylancl 587 . . . . . 6 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥}))
27 vsnex 5390 . . . . . . . 8 {𝑥} ∈ V
2827pwex 5339 . . . . . . 7 𝒫 {𝑥} ∈ V
29 uncom 4117 . . . . . . . . 9 ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = ({𝑥} ∪ (𝐴 ∖ {𝑥}))
30 simpr 486 . . . . . . . . . . 11 ((1o𝐴𝑥𝐴) → 𝑥𝐴)
3130snssd 4773 . . . . . . . . . 10 ((1o𝐴𝑥𝐴) → {𝑥} ⊆ 𝐴)
32 undif 4445 . . . . . . . . . 10 ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴)
3331, 32sylib 217 . . . . . . . . 9 ((1o𝐴𝑥𝐴) → ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴)
3429, 33eqtrid 2785 . . . . . . . 8 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = 𝐴)
3512difexd 5290 . . . . . . . . 9 ((1o𝐴𝑥𝐴) → (𝐴 ∖ {𝑥}) ∈ V)
36 canth2g 9081 . . . . . . . . 9 ((𝐴 ∖ {𝑥}) ∈ V → (𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}))
37 domunsn 9077 . . . . . . . . 9 ((𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥}))
3835, 36, 373syl 18 . . . . . . . 8 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥}))
3934, 38eqbrtrrd 5133 . . . . . . 7 ((1o𝐴𝑥𝐴) → 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥}))
40 xpdom1g 9019 . . . . . . 7 ((𝒫 {𝑥} ∈ V ∧ 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥})) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4128, 39, 40sylancr 588 . . . . . 6 ((1o𝐴𝑥𝐴) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
42 endomtr 8958 . . . . . 6 (((𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥}) ∧ (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) → (𝐴 × 2o) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4326, 41, 42syl2anc 585 . . . . 5 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
44 pwdjuen 10125 . . . . . . 7 (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4535, 27, 44sylancl 587 . . . . . 6 ((1o𝐴𝑥𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4645ensymd 8951 . . . . 5 ((1o𝐴𝑥𝐴) → (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}))
47 domentr 8959 . . . . 5 (((𝐴 × 2o) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ∧ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) → (𝐴 × 2o) ≼ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}))
4843, 46, 47syl2anc 585 . . . 4 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≼ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}))
4927a1i 11 . . . . . . 7 ((1o𝐴𝑥𝐴) → {𝑥} ∈ V)
50 disjdifr 4436 . . . . . . . 8 ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅
5150a1i 11 . . . . . . 7 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅)
52 endjudisj 10112 . . . . . . 7 (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V ∧ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥}))
5335, 49, 51, 52syl3anc 1372 . . . . . 6 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥}))
5453, 34breqtrd 5135 . . . . 5 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴)
55 pwen 9100 . . . . 5 (((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴 → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴)
5654, 55syl 17 . . . 4 ((1o𝐴𝑥𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴)
57 domentr 8959 . . . 4 (((𝐴 × 2o) ≼ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ∧ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) → (𝐴 × 2o) ≼ 𝒫 𝐴)
5848, 56, 57syl2anc 585 . . 3 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≼ 𝒫 𝐴)
599, 58exlimddv 1939 . 2 (1o𝐴 → (𝐴 × 2o) ≼ 𝒫 𝐴)
60 domtr 8953 . 2 (((𝐴 ⊔ 2o) ≼ (𝐴 × 2o) ∧ (𝐴 × 2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
613, 59, 60syl2anc 585 1 (1o𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wex 1782  wcel 2107  Vcvv 3447  cdif 3911  cun 3912  cin 3913  wss 3914  c0 4286  𝒫 cpw 4564  {csn 4590  {cpr 4592   class class class wbr 5109   × cxp 5635  1oc1o 8409  2oc2o 8410  cen 8886  cdom 8887  csdm 8888  cdju 9842
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 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
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 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-dju 9845
This theorem is referenced by:  canthp1lem2  10597  canthp1  10598
  Copyright terms: Public domain W3C validator