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

Theorem sucdom2 8755
Description: Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
Assertion
Ref Expression
sucdom2 (𝐴𝐵 → suc 𝐴𝐵)

Proof of Theorem sucdom2
Dummy variables 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sdomdom 8656 . . 3 (𝐴𝐵𝐴𝐵)
2 brdomi 8639 . . 3 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
4 relsdom 8633 . . . . . . 7 Rel ≺
54brrelex1i 5605 . . . . . 6 (𝐴𝐵𝐴 ∈ V)
65adantr 484 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐴 ∈ V)
7 vex 3412 . . . . . . 7 𝑓 ∈ V
87rnex 7690 . . . . . 6 ran 𝑓 ∈ V
98a1i 11 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ran 𝑓 ∈ V)
10 f1f1orn 6672 . . . . . . 7 (𝑓:𝐴1-1𝐵𝑓:𝐴1-1-onto→ran 𝑓)
1110adantl 485 . . . . . 6 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝑓:𝐴1-1-onto→ran 𝑓)
12 f1of1 6660 . . . . . 6 (𝑓:𝐴1-1-onto→ran 𝑓𝑓:𝐴1-1→ran 𝑓)
1311, 12syl 17 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝑓:𝐴1-1→ran 𝑓)
14 f1dom2g 8646 . . . . 5 ((𝐴 ∈ V ∧ ran 𝑓 ∈ V ∧ 𝑓:𝐴1-1→ran 𝑓) → 𝐴 ≼ ran 𝑓)
156, 9, 13, 14syl3anc 1373 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐴 ≼ ran 𝑓)
16 sdomnen 8657 . . . . . . . 8 (𝐴𝐵 → ¬ 𝐴𝐵)
1716adantr 484 . . . . . . 7 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ¬ 𝐴𝐵)
18 ssdif0 4278 . . . . . . . 8 (𝐵 ⊆ ran 𝑓 ↔ (𝐵 ∖ ran 𝑓) = ∅)
19 simplr 769 . . . . . . . . . . 11 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝑓:𝐴1-1𝐵)
20 f1f 6615 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
2120frnd 6553 . . . . . . . . . . . . 13 (𝑓:𝐴1-1𝐵 → ran 𝑓𝐵)
2219, 21syl 17 . . . . . . . . . . . 12 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → ran 𝑓𝐵)
23 simpr 488 . . . . . . . . . . . 12 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝐵 ⊆ ran 𝑓)
2422, 23eqssd 3918 . . . . . . . . . . 11 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → ran 𝑓 = 𝐵)
25 dff1o5 6670 . . . . . . . . . . 11 (𝑓:𝐴1-1-onto𝐵 ↔ (𝑓:𝐴1-1𝐵 ∧ ran 𝑓 = 𝐵))
2619, 24, 25sylanbrc 586 . . . . . . . . . 10 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝑓:𝐴1-1-onto𝐵)
27 f1oen3g 8644 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:𝐴1-1-onto𝐵) → 𝐴𝐵)
287, 26, 27sylancr 590 . . . . . . . . 9 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝐴𝐵)
2928ex 416 . . . . . . . 8 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐵 ⊆ ran 𝑓𝐴𝐵))
3018, 29syl5bir 246 . . . . . . 7 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ((𝐵 ∖ ran 𝑓) = ∅ → 𝐴𝐵))
3117, 30mtod 201 . . . . . 6 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ¬ (𝐵 ∖ ran 𝑓) = ∅)
32 neq0 4260 . . . . . 6 (¬ (𝐵 ∖ ran 𝑓) = ∅ ↔ ∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓))
3331, 32sylib 221 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓))
34 snssi 4721 . . . . . . 7 (𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝑤} ⊆ (𝐵 ∖ ran 𝑓))
35 vex 3412 . . . . . . . . 9 𝑤 ∈ V
36 en2sn 8718 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝑤 ∈ V) → {𝐴} ≈ {𝑤})
376, 35, 36sylancl 589 . . . . . . . 8 ((𝐴𝐵𝑓:𝐴1-1𝐵) → {𝐴} ≈ {𝑤})
384brrelex2i 5606 . . . . . . . . . 10 (𝐴𝐵𝐵 ∈ V)
3938adantr 484 . . . . . . . . 9 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐵 ∈ V)
40 difexg 5220 . . . . . . . . 9 (𝐵 ∈ V → (𝐵 ∖ ran 𝑓) ∈ V)
41 ssdomg 8674 . . . . . . . . 9 ((𝐵 ∖ ran 𝑓) ∈ V → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝑤} ≼ (𝐵 ∖ ran 𝑓)))
4239, 40, 413syl 18 . . . . . . . 8 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝑤} ≼ (𝐵 ∖ ran 𝑓)))
43 endomtr 8686 . . . . . . . 8 (({𝐴} ≈ {𝑤} ∧ {𝑤} ≼ (𝐵 ∖ ran 𝑓)) → {𝐴} ≼ (𝐵 ∖ ran 𝑓))
4437, 42, 43syl6an 684 . . . . . . 7 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
4534, 44syl5 34 . . . . . 6 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
4645exlimdv 1941 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
4733, 46mpd 15 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → {𝐴} ≼ (𝐵 ∖ ran 𝑓))
48 disjdif 4386 . . . . 5 (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅
4948a1i 11 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅)
50 undom 8733 . . . 4 (((𝐴 ≼ ran 𝑓 ∧ {𝐴} ≼ (𝐵 ∖ ran 𝑓)) ∧ (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅) → (𝐴 ∪ {𝐴}) ≼ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
5115, 47, 49, 50syl21anc 838 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐴 ∪ {𝐴}) ≼ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
52 df-suc 6219 . . . 4 suc 𝐴 = (𝐴 ∪ {𝐴})
5352a1i 11 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → suc 𝐴 = (𝐴 ∪ {𝐴}))
54 undif2 4391 . . . 4 (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)) = (ran 𝑓𝐵)
5521adantl 485 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ran 𝑓𝐵)
56 ssequn1 4094 . . . . 5 (ran 𝑓𝐵 ↔ (ran 𝑓𝐵) = 𝐵)
5755, 56sylib 221 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (ran 𝑓𝐵) = 𝐵)
5854, 57eqtr2id 2791 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐵 = (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
5951, 53, 583brtr4d 5085 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → suc 𝐴𝐵)
603, 59exlimddv 1943 1 (𝐴𝐵 → suc 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1543  wex 1787  wcel 2110  Vcvv 3408  cdif 3863  cun 3864  cin 3865  wss 3866  c0 4237  {csn 4541   class class class wbr 5053  ran crn 5552  suc csuc 6215  1-1wf1 6377  1-1-ontowf1o 6379  cen 8623  cdom 8624  csdm 8625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-suc 6219  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-en 8627  df-dom 8628  df-sdom 8629
This theorem is referenced by:  sucdom  8875  card2inf  9171
  Copyright terms: Public domain W3C validator