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

Theorem sucdom2OLD 9121
Description: Obsolete version of sucdom2 9241 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sucdom2OLD (𝐴𝐵 → suc 𝐴𝐵)

Proof of Theorem sucdom2OLD
Dummy variables 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sdomdom 9019 . . 3 (𝐴𝐵𝐴𝐵)
2 brdomi 8998 . . 3 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
4 relsdom 8991 . . . . . . 7 Rel ≺
54brrelex1i 5745 . . . . . 6 (𝐴𝐵𝐴 ∈ V)
65adantr 480 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐴 ∈ V)
7 vex 3482 . . . . . . 7 𝑓 ∈ V
87rnex 7933 . . . . . 6 ran 𝑓 ∈ V
98a1i 11 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ran 𝑓 ∈ V)
10 f1f1orn 6860 . . . . . . 7 (𝑓:𝐴1-1𝐵𝑓:𝐴1-1-onto→ran 𝑓)
1110adantl 481 . . . . . 6 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝑓:𝐴1-1-onto→ran 𝑓)
12 f1of1 6848 . . . . . 6 (𝑓:𝐴1-1-onto→ran 𝑓𝑓:𝐴1-1→ran 𝑓)
1311, 12syl 17 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝑓:𝐴1-1→ran 𝑓)
14 f1dom2g 9009 . . . . 5 ((𝐴 ∈ V ∧ ran 𝑓 ∈ V ∧ 𝑓:𝐴1-1→ran 𝑓) → 𝐴 ≼ ran 𝑓)
156, 9, 13, 14syl3anc 1370 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐴 ≼ ran 𝑓)
16 sdomnen 9020 . . . . . . . 8 (𝐴𝐵 → ¬ 𝐴𝐵)
1716adantr 480 . . . . . . 7 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ¬ 𝐴𝐵)
18 ssdif0 4372 . . . . . . . 8 (𝐵 ⊆ ran 𝑓 ↔ (𝐵 ∖ ran 𝑓) = ∅)
19 simplr 769 . . . . . . . . . . 11 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝑓:𝐴1-1𝐵)
20 f1f 6805 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
2120frnd 6745 . . . . . . . . . . . . 13 (𝑓:𝐴1-1𝐵 → ran 𝑓𝐵)
2219, 21syl 17 . . . . . . . . . . . 12 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → ran 𝑓𝐵)
23 simpr 484 . . . . . . . . . . . 12 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝐵 ⊆ ran 𝑓)
2422, 23eqssd 4013 . . . . . . . . . . 11 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → ran 𝑓 = 𝐵)
25 dff1o5 6858 . . . . . . . . . . 11 (𝑓:𝐴1-1-onto𝐵 ↔ (𝑓:𝐴1-1𝐵 ∧ ran 𝑓 = 𝐵))
2619, 24, 25sylanbrc 583 . . . . . . . . . 10 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝑓:𝐴1-1-onto𝐵)
27 f1oen3g 9006 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:𝐴1-1-onto𝐵) → 𝐴𝐵)
287, 26, 27sylancr 587 . . . . . . . . 9 (((𝐴𝐵𝑓:𝐴1-1𝐵) ∧ 𝐵 ⊆ ran 𝑓) → 𝐴𝐵)
2928ex 412 . . . . . . . 8 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐵 ⊆ ran 𝑓𝐴𝐵))
3018, 29biimtrrid 243 . . . . . . 7 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ((𝐵 ∖ ran 𝑓) = ∅ → 𝐴𝐵))
3117, 30mtod 198 . . . . . 6 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ¬ (𝐵 ∖ ran 𝑓) = ∅)
32 neq0 4358 . . . . . 6 (¬ (𝐵 ∖ ran 𝑓) = ∅ ↔ ∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓))
3331, 32sylib 218 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓))
34 snssi 4813 . . . . . . 7 (𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝑤} ⊆ (𝐵 ∖ ran 𝑓))
35 vex 3482 . . . . . . . . 9 𝑤 ∈ V
36 en2sn 9080 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝑤 ∈ V) → {𝐴} ≈ {𝑤})
376, 35, 36sylancl 586 . . . . . . . 8 ((𝐴𝐵𝑓:𝐴1-1𝐵) → {𝐴} ≈ {𝑤})
384brrelex2i 5746 . . . . . . . . . 10 (𝐴𝐵𝐵 ∈ V)
3938adantr 480 . . . . . . . . 9 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐵 ∈ V)
40 difexg 5335 . . . . . . . . 9 (𝐵 ∈ V → (𝐵 ∖ ran 𝑓) ∈ V)
41 ssdomg 9039 . . . . . . . . 9 ((𝐵 ∖ ran 𝑓) ∈ V → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝑤} ≼ (𝐵 ∖ ran 𝑓)))
4239, 40, 413syl 18 . . . . . . . 8 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝑤} ≼ (𝐵 ∖ ran 𝑓)))
43 endomtr 9051 . . . . . . . 8 (({𝐴} ≈ {𝑤} ∧ {𝑤} ≼ (𝐵 ∖ ran 𝑓)) → {𝐴} ≼ (𝐵 ∖ ran 𝑓))
4437, 42, 43syl6an 684 . . . . . . 7 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ({𝑤} ⊆ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
4534, 44syl5 34 . . . . . 6 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
4645exlimdv 1931 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (∃𝑤 𝑤 ∈ (𝐵 ∖ ran 𝑓) → {𝐴} ≼ (𝐵 ∖ ran 𝑓)))
4733, 46mpd 15 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → {𝐴} ≼ (𝐵 ∖ ran 𝑓))
48 disjdif 4478 . . . . 5 (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅
4948a1i 11 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅)
50 undom 9098 . . . 4 (((𝐴 ≼ ran 𝑓 ∧ {𝐴} ≼ (𝐵 ∖ ran 𝑓)) ∧ (ran 𝑓 ∩ (𝐵 ∖ ran 𝑓)) = ∅) → (𝐴 ∪ {𝐴}) ≼ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
5115, 47, 49, 50syl21anc 838 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐴 ∪ {𝐴}) ≼ (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
52 df-suc 6392 . . . 4 suc 𝐴 = (𝐴 ∪ {𝐴})
5352a1i 11 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → suc 𝐴 = (𝐴 ∪ {𝐴}))
54 undif2 4483 . . . 4 (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)) = (ran 𝑓𝐵)
5521adantl 481 . . . . 5 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ran 𝑓𝐵)
56 ssequn1 4196 . . . . 5 (ran 𝑓𝐵 ↔ (ran 𝑓𝐵) = 𝐵)
5755, 56sylib 218 . . . 4 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (ran 𝑓𝐵) = 𝐵)
5854, 57eqtr2id 2788 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → 𝐵 = (ran 𝑓 ∪ (𝐵 ∖ ran 𝑓)))
5951, 53, 583brtr4d 5180 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → suc 𝐴𝐵)
603, 59exlimddv 1933 1 (𝐴𝐵 → suc 𝐴𝐵)
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  ran crn 5690  suc csuc 6388  1-1wf1 6560  1-1-ontowf1o 6562  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-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-suc 6392  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: (None)
  Copyright terms: Public domain W3C validator