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

Theorem domdifsn 8210
Description: Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
domdifsn (𝐴𝐵𝐴 ≼ (𝐵 ∖ {𝐶}))

Proof of Theorem domdifsn
Dummy variables 𝑓 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sdomdom 8151 . . . . 5 (𝐴𝐵𝐴𝐵)
2 relsdom 8130 . . . . . . 7 Rel ≺
32brrelex2i 5316 . . . . . 6 (𝐴𝐵𝐵 ∈ V)
4 brdomg 8133 . . . . . 6 (𝐵 ∈ V → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))
53, 4syl 17 . . . . 5 (𝐴𝐵 → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))
61, 5mpbid 222 . . . 4 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
76adantr 472 . . 3 ((𝐴𝐵𝐶𝐵) → ∃𝑓 𝑓:𝐴1-1𝐵)
8 f1f 6262 . . . . . . . 8 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
9 frn 6214 . . . . . . . 8 (𝑓:𝐴𝐵 → ran 𝑓𝐵)
108, 9syl 17 . . . . . . 7 (𝑓:𝐴1-1𝐵 → ran 𝑓𝐵)
1110adantl 473 . . . . . 6 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → ran 𝑓𝐵)
12 sdomnen 8152 . . . . . . . 8 (𝐴𝐵 → ¬ 𝐴𝐵)
1312ad2antrr 764 . . . . . . 7 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → ¬ 𝐴𝐵)
14 vex 3343 . . . . . . . . . . 11 𝑓 ∈ V
15 dff1o5 6308 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto𝐵 ↔ (𝑓:𝐴1-1𝐵 ∧ ran 𝑓 = 𝐵))
1615biimpri 218 . . . . . . . . . . 11 ((𝑓:𝐴1-1𝐵 ∧ ran 𝑓 = 𝐵) → 𝑓:𝐴1-1-onto𝐵)
17 f1oen3g 8139 . . . . . . . . . . 11 ((𝑓 ∈ V ∧ 𝑓:𝐴1-1-onto𝐵) → 𝐴𝐵)
1814, 16, 17sylancr 698 . . . . . . . . . 10 ((𝑓:𝐴1-1𝐵 ∧ ran 𝑓 = 𝐵) → 𝐴𝐵)
1918ex 449 . . . . . . . . 9 (𝑓:𝐴1-1𝐵 → (ran 𝑓 = 𝐵𝐴𝐵))
2019necon3bd 2946 . . . . . . . 8 (𝑓:𝐴1-1𝐵 → (¬ 𝐴𝐵 → ran 𝑓𝐵))
2120adantl 473 . . . . . . 7 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → (¬ 𝐴𝐵 → ran 𝑓𝐵))
2213, 21mpd 15 . . . . . 6 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → ran 𝑓𝐵)
23 pssdifn0 4087 . . . . . 6 ((ran 𝑓𝐵 ∧ ran 𝑓𝐵) → (𝐵 ∖ ran 𝑓) ≠ ∅)
2411, 22, 23syl2anc 696 . . . . 5 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → (𝐵 ∖ ran 𝑓) ≠ ∅)
25 n0 4074 . . . . 5 ((𝐵 ∖ ran 𝑓) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ ran 𝑓))
2624, 25sylib 208 . . . 4 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → ∃𝑥 𝑥 ∈ (𝐵 ∖ ran 𝑓))
272brrelexi 5315 . . . . . . . . 9 (𝐴𝐵𝐴 ∈ V)
2827ad2antrr 764 . . . . . . . 8 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝐴 ∈ V)
293ad2antrr 764 . . . . . . . . 9 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝐵 ∈ V)
30 difexg 4960 . . . . . . . . 9 (𝐵 ∈ V → (𝐵 ∖ {𝑥}) ∈ V)
3129, 30syl 17 . . . . . . . 8 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → (𝐵 ∖ {𝑥}) ∈ V)
32 eldifn 3876 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐵 ∖ ran 𝑓) → ¬ 𝑥 ∈ ran 𝑓)
33 disjsn 4390 . . . . . . . . . . . . 13 ((ran 𝑓 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ran 𝑓)
3432, 33sylibr 224 . . . . . . . . . . . 12 (𝑥 ∈ (𝐵 ∖ ran 𝑓) → (ran 𝑓 ∩ {𝑥}) = ∅)
3534adantl 473 . . . . . . . . . . 11 ((𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓)) → (ran 𝑓 ∩ {𝑥}) = ∅)
3610adantr 472 . . . . . . . . . . . 12 ((𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓)) → ran 𝑓𝐵)
37 reldisj 4163 . . . . . . . . . . . 12 (ran 𝑓𝐵 → ((ran 𝑓 ∩ {𝑥}) = ∅ ↔ ran 𝑓 ⊆ (𝐵 ∖ {𝑥})))
3836, 37syl 17 . . . . . . . . . . 11 ((𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓)) → ((ran 𝑓 ∩ {𝑥}) = ∅ ↔ ran 𝑓 ⊆ (𝐵 ∖ {𝑥})))
3935, 38mpbid 222 . . . . . . . . . 10 ((𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓)) → ran 𝑓 ⊆ (𝐵 ∖ {𝑥}))
40 f1ssr 6268 . . . . . . . . . 10 ((𝑓:𝐴1-1𝐵 ∧ ran 𝑓 ⊆ (𝐵 ∖ {𝑥})) → 𝑓:𝐴1-1→(𝐵 ∖ {𝑥}))
4139, 40syldan 488 . . . . . . . . 9 ((𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓)) → 𝑓:𝐴1-1→(𝐵 ∖ {𝑥}))
4241adantl 473 . . . . . . . 8 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝑓:𝐴1-1→(𝐵 ∖ {𝑥}))
43 f1dom2g 8141 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝐵 ∖ {𝑥}) ∈ V ∧ 𝑓:𝐴1-1→(𝐵 ∖ {𝑥})) → 𝐴 ≼ (𝐵 ∖ {𝑥}))
4428, 31, 42, 43syl3anc 1477 . . . . . . 7 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝐴 ≼ (𝐵 ∖ {𝑥}))
45 eldifi 3875 . . . . . . . . 9 (𝑥 ∈ (𝐵 ∖ ran 𝑓) → 𝑥𝐵)
4645ad2antll 767 . . . . . . . 8 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝑥𝐵)
47 simplr 809 . . . . . . . 8 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝐶𝐵)
48 difsnen 8209 . . . . . . . 8 ((𝐵 ∈ V ∧ 𝑥𝐵𝐶𝐵) → (𝐵 ∖ {𝑥}) ≈ (𝐵 ∖ {𝐶}))
4929, 46, 47, 48syl3anc 1477 . . . . . . 7 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → (𝐵 ∖ {𝑥}) ≈ (𝐵 ∖ {𝐶}))
50 domentr 8182 . . . . . . 7 ((𝐴 ≼ (𝐵 ∖ {𝑥}) ∧ (𝐵 ∖ {𝑥}) ≈ (𝐵 ∖ {𝐶})) → 𝐴 ≼ (𝐵 ∖ {𝐶}))
5144, 49, 50syl2anc 696 . . . . . 6 (((𝐴𝐵𝐶𝐵) ∧ (𝑓:𝐴1-1𝐵𝑥 ∈ (𝐵 ∖ ran 𝑓))) → 𝐴 ≼ (𝐵 ∖ {𝐶}))
5251expr 644 . . . . 5 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → (𝑥 ∈ (𝐵 ∖ ran 𝑓) → 𝐴 ≼ (𝐵 ∖ {𝐶})))
5352exlimdv 2010 . . . 4 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → (∃𝑥 𝑥 ∈ (𝐵 ∖ ran 𝑓) → 𝐴 ≼ (𝐵 ∖ {𝐶})))
5426, 53mpd 15 . . 3 (((𝐴𝐵𝐶𝐵) ∧ 𝑓:𝐴1-1𝐵) → 𝐴 ≼ (𝐵 ∖ {𝐶}))
557, 54exlimddv 2012 . 2 ((𝐴𝐵𝐶𝐵) → 𝐴 ≼ (𝐵 ∖ {𝐶}))
561adantr 472 . . 3 ((𝐴𝐵 ∧ ¬ 𝐶𝐵) → 𝐴𝐵)
57 difsn 4473 . . . . 5 𝐶𝐵 → (𝐵 ∖ {𝐶}) = 𝐵)
5857breq2d 4816 . . . 4 𝐶𝐵 → (𝐴 ≼ (𝐵 ∖ {𝐶}) ↔ 𝐴𝐵))
5958adantl 473 . . 3 ((𝐴𝐵 ∧ ¬ 𝐶𝐵) → (𝐴 ≼ (𝐵 ∖ {𝐶}) ↔ 𝐴𝐵))
6056, 59mpbird 247 . 2 ((𝐴𝐵 ∧ ¬ 𝐶𝐵) → 𝐴 ≼ (𝐵 ∖ {𝐶}))
6155, 60pm2.61dan 867 1 (𝐴𝐵𝐴 ≼ (𝐵 ∖ {𝐶}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1632  wex 1853  wcel 2139  wne 2932  Vcvv 3340  cdif 3712  cin 3714  wss 3715  c0 4058  {csn 4321   class class class wbr 4804  ran crn 5267  wf 6045  1-1wf1 6046  1-1-ontowf1o 6048  cen 8120  cdom 8121  csdm 8122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-suc 5890  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-1o 7730  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126
This theorem is referenced by:  domunsn  8277  marypha1lem  8506
  Copyright terms: Public domain W3C validator