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

Theorem domunsn 9166
Description: Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.)
Assertion
Ref Expression
domunsn (𝐴𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵)

Proof of Theorem domunsn
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 sdom0 9147 . . . . 5 ¬ 𝐴 ≺ ∅
2 breq2 5152 . . . . 5 (𝐵 = ∅ → (𝐴𝐵𝐴 ≺ ∅))
31, 2mtbiri 327 . . . 4 (𝐵 = ∅ → ¬ 𝐴𝐵)
43con2i 139 . . 3 (𝐴𝐵 → ¬ 𝐵 = ∅)
5 neq0 4358 . . 3 𝐵 = ∅ ↔ ∃𝑧 𝑧𝐵)
64, 5sylib 218 . 2 (𝐴𝐵 → ∃𝑧 𝑧𝐵)
7 domdifsn 9093 . . . . 5 (𝐴𝐵𝐴 ≼ (𝐵 ∖ {𝑧}))
87adantr 480 . . . 4 ((𝐴𝐵𝑧𝐵) → 𝐴 ≼ (𝐵 ∖ {𝑧}))
9 en2sn 9080 . . . . . . 7 ((𝐶 ∈ V ∧ 𝑧 ∈ V) → {𝐶} ≈ {𝑧})
109elvd 3484 . . . . . 6 (𝐶 ∈ V → {𝐶} ≈ {𝑧})
11 endom 9018 . . . . . 6 ({𝐶} ≈ {𝑧} → {𝐶} ≼ {𝑧})
1210, 11syl 17 . . . . 5 (𝐶 ∈ V → {𝐶} ≼ {𝑧})
13 snprc 4722 . . . . . . 7 𝐶 ∈ V ↔ {𝐶} = ∅)
1413biimpi 216 . . . . . 6 𝐶 ∈ V → {𝐶} = ∅)
15 vsnex 5440 . . . . . . 7 {𝑧} ∈ V
16150dom 9145 . . . . . 6 ∅ ≼ {𝑧}
1714, 16eqbrtrdi 5187 . . . . 5 𝐶 ∈ V → {𝐶} ≼ {𝑧})
1812, 17pm2.61i 182 . . . 4 {𝐶} ≼ {𝑧}
19 disjdifr 4479 . . . . 5 ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ∅
20 undom 9098 . . . . 5 (((𝐴 ≼ (𝐵 ∖ {𝑧}) ∧ {𝐶} ≼ {𝑧}) ∧ ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧}))
2119, 20mpan2 691 . . . 4 ((𝐴 ≼ (𝐵 ∖ {𝑧}) ∧ {𝐶} ≼ {𝑧}) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧}))
228, 18, 21sylancl 586 . . 3 ((𝐴𝐵𝑧𝐵) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧}))
23 uncom 4168 . . . 4 ((𝐵 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝐵 ∖ {𝑧}))
24 simpr 484 . . . . . 6 ((𝐴𝐵𝑧𝐵) → 𝑧𝐵)
2524snssd 4814 . . . . 5 ((𝐴𝐵𝑧𝐵) → {𝑧} ⊆ 𝐵)
26 undif 4488 . . . . 5 ({𝑧} ⊆ 𝐵 ↔ ({𝑧} ∪ (𝐵 ∖ {𝑧})) = 𝐵)
2725, 26sylib 218 . . . 4 ((𝐴𝐵𝑧𝐵) → ({𝑧} ∪ (𝐵 ∖ {𝑧})) = 𝐵)
2823, 27eqtrid 2787 . . 3 ((𝐴𝐵𝑧𝐵) → ((𝐵 ∖ {𝑧}) ∪ {𝑧}) = 𝐵)
2922, 28breqtrd 5174 . 2 ((𝐴𝐵𝑧𝐵) → (𝐴 ∪ {𝐶}) ≼ 𝐵)
306, 29exlimddv 1933 1 (𝐴𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1537  wex 1776  wcel 2106  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  {csn 4631   class class class wbr 5148  cen 8981  cdom 8982  csdm 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-en 8985  df-dom 8986  df-sdom 8987
This theorem is referenced by:  canthp1lem1  10690
  Copyright terms: Public domain W3C validator