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

Theorem canthp1lem1 10588
Description: Lemma for canthp1 10590. (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 9184 . . 3 1o ≺ 2o
2 djuxpdom 10121 . . 3 ((1o𝐴 ∧ 1o ≺ 2o) → (𝐴 ⊔ 2o) ≼ (𝐴 × 2o))
31, 2mpan2 689 . 2 (1o𝐴 → (𝐴 ⊔ 2o) ≼ (𝐴 × 2o))
4 sdom0 9052 . . . . . 6 ¬ 1o ≺ ∅
5 breq2 5109 . . . . . 6 (𝐴 = ∅ → (1o𝐴 ↔ 1o ≺ ∅))
64, 5mtbiri 326 . . . . 5 (𝐴 = ∅ → ¬ 1o𝐴)
76con2i 139 . . . 4 (1o𝐴 → ¬ 𝐴 = ∅)
8 neq0 4305 . . . 4 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
97, 8sylib 217 . . 3 (1o𝐴 → ∃𝑥 𝑥𝐴)
10 relsdom 8890 . . . . . . . . . 10 Rel ≺
1110brrelex2i 5689 . . . . . . . . 9 (1o𝐴𝐴 ∈ V)
1211adantr 481 . . . . . . . 8 ((1o𝐴𝑥𝐴) → 𝐴 ∈ V)
13 enrefg 8924 . . . . . . . 8 (𝐴 ∈ V → 𝐴𝐴)
1412, 13syl 17 . . . . . . 7 ((1o𝐴𝑥𝐴) → 𝐴𝐴)
15 df2o2 8421 . . . . . . . . 9 2o = {∅, {∅}}
16 pwpw0 4773 . . . . . . . . 9 𝒫 {∅} = {∅, {∅}}
1715, 16eqtr4i 2767 . . . . . . . 8 2o = 𝒫 {∅}
18 0ex 5264 . . . . . . . . . 10 ∅ ∈ V
19 vex 3449 . . . . . . . . . 10 𝑥 ∈ V
20 en2sn 8985 . . . . . . . . . 10 ((∅ ∈ V ∧ 𝑥 ∈ V) → {∅} ≈ {𝑥})
2118, 19, 20mp2an 690 . . . . . . . . 9 {∅} ≈ {𝑥}
22 pwen 9094 . . . . . . . . 9 ({∅} ≈ {𝑥} → 𝒫 {∅} ≈ 𝒫 {𝑥})
2321, 22ax-mp 5 . . . . . . . 8 𝒫 {∅} ≈ 𝒫 {𝑥}
2417, 23eqbrtri 5126 . . . . . . 7 2o ≈ 𝒫 {𝑥}
25 xpen 9084 . . . . . . 7 ((𝐴𝐴 ∧ 2o ≈ 𝒫 {𝑥}) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥}))
2614, 24, 25sylancl 586 . . . . . 6 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥}))
27 vsnex 5386 . . . . . . . 8 {𝑥} ∈ V
2827pwex 5335 . . . . . . 7 𝒫 {𝑥} ∈ V
29 uncom 4113 . . . . . . . . 9 ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = ({𝑥} ∪ (𝐴 ∖ {𝑥}))
30 simpr 485 . . . . . . . . . . 11 ((1o𝐴𝑥𝐴) → 𝑥𝐴)
3130snssd 4769 . . . . . . . . . 10 ((1o𝐴𝑥𝐴) → {𝑥} ⊆ 𝐴)
32 undif 4441 . . . . . . . . . 10 ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴)
3331, 32sylib 217 . . . . . . . . 9 ((1o𝐴𝑥𝐴) → ({𝑥} ∪ (𝐴 ∖ {𝑥})) = 𝐴)
3429, 33eqtrid 2788 . . . . . . . 8 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = 𝐴)
3512difexd 5286 . . . . . . . . 9 ((1o𝐴𝑥𝐴) → (𝐴 ∖ {𝑥}) ∈ V)
36 canth2g 9075 . . . . . . . . 9 ((𝐴 ∖ {𝑥}) ∈ V → (𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}))
37 domunsn 9071 . . . . . . . . 9 ((𝐴 ∖ {𝑥}) ≺ 𝒫 (𝐴 ∖ {𝑥}) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥}))
3835, 36, 373syl 18 . . . . . . . 8 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ≼ 𝒫 (𝐴 ∖ {𝑥}))
3934, 38eqbrtrrd 5129 . . . . . . 7 ((1o𝐴𝑥𝐴) → 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥}))
40 xpdom1g 9013 . . . . . . 7 ((𝒫 {𝑥} ∈ V ∧ 𝐴 ≼ 𝒫 (𝐴 ∖ {𝑥})) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4128, 39, 40sylancr 587 . . . . . 6 ((1o𝐴𝑥𝐴) → (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
42 endomtr 8952 . . . . . 6 (((𝐴 × 2o) ≈ (𝐴 × 𝒫 {𝑥}) ∧ (𝐴 × 𝒫 {𝑥}) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥})) → (𝐴 × 2o) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4326, 41, 42syl2anc 584 . . . . 5 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
44 pwdjuen 10117 . . . . . . 7 (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4535, 27, 44sylancl 586 . . . . . 6 ((1o𝐴𝑥𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}))
4645ensymd 8945 . . . . 5 ((1o𝐴𝑥𝐴) → (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}))
47 domentr 8953 . . . . 5 (((𝐴 × 2o) ≼ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ∧ (𝒫 (𝐴 ∖ {𝑥}) × 𝒫 {𝑥}) ≈ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥})) → (𝐴 × 2o) ≼ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}))
4843, 46, 47syl2anc 584 . . . 4 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≼ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}))
4927a1i 11 . . . . . . 7 ((1o𝐴𝑥𝐴) → {𝑥} ∈ V)
50 disjdifr 4432 . . . . . . . 8 ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅
5150a1i 11 . . . . . . 7 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅)
52 endjudisj 10104 . . . . . . 7 (((𝐴 ∖ {𝑥}) ∈ V ∧ {𝑥} ∈ V ∧ ((𝐴 ∖ {𝑥}) ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥}))
5335, 49, 51, 52syl3anc 1371 . . . . . 6 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ ((𝐴 ∖ {𝑥}) ∪ {𝑥}))
5453, 34breqtrd 5131 . . . . 5 ((1o𝐴𝑥𝐴) → ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴)
55 pwen 9094 . . . . 5 (((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝐴 → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴)
5654, 55syl 17 . . . 4 ((1o𝐴𝑥𝐴) → 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴)
57 domentr 8953 . . . 4 (((𝐴 × 2o) ≼ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ∧ 𝒫 ((𝐴 ∖ {𝑥}) ⊔ {𝑥}) ≈ 𝒫 𝐴) → (𝐴 × 2o) ≼ 𝒫 𝐴)
5848, 56, 57syl2anc 584 . . 3 ((1o𝐴𝑥𝐴) → (𝐴 × 2o) ≼ 𝒫 𝐴)
599, 58exlimddv 1938 . 2 (1o𝐴 → (𝐴 × 2o) ≼ 𝒫 𝐴)
60 domtr 8947 . 2 (((𝐴 ⊔ 2o) ≼ (𝐴 × 2o) ∧ (𝐴 × 2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
613, 59, 60syl2anc 584 1 (1o𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wex 1781  wcel 2106  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586  {cpr 4588   class class class wbr 5105   × cxp 5631  1oc1o 8405  2oc2o 8406  cen 8880  cdom 8881  csdm 8882  cdju 9834
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-dju 9837
This theorem is referenced by:  canthp1lem2  10589  canthp1  10590
  Copyright terms: Public domain W3C validator