MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sucdom2 Structured version   Visualization version   GIF version
Theorem sucdom2 9206
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.) Avoid ax-pow 5364. (Revised by BTernaryTau, 4-Dec-2024.)
Assertion
Ref Expression
sucdom2 (𝐴 β‰Ί 𝐡 β†’ suc 𝐴 β‰Ό 𝐡)
Proof of Theorem sucdom2
Dummy variables 𝑓 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sdomdom 8976 . . 3 (𝐴 β‰Ί 𝐡 β†’ 𝐴 β‰Ό 𝐡)
2 brdomi 8954 . . 3 (𝐴 β‰Ό 𝐡 β†’ βˆƒπ‘“ 𝑓:𝐴–1-1→𝐡)
31, 2syl 17 . 2 (𝐴 β‰Ί 𝐡 β†’ βˆƒπ‘“ 𝑓:𝐴–1-1→𝐡)
4 vex 3479 . . . . 5 𝑓 ∈ V
54rnex 7903 . . . . 5 ran 𝑓 ∈ V
6 f1f1orn 6845 . . . . . . 7 (𝑓:𝐴–1-1→𝐡 β†’ 𝑓:𝐴–1-1-ontoβ†’ran 𝑓)
76adantl 483 . . . . . 6 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ 𝑓:𝐴–1-1-ontoβ†’ran 𝑓)
8 f1of1 6833 . . . . . 6 (𝑓:𝐴–1-1-ontoβ†’ran 𝑓 β†’ 𝑓:𝐴–1-1β†’ran 𝑓)
97, 8syl 17 . . . . 5 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ 𝑓:𝐴–1-1β†’ran 𝑓)
10 f1dom3g 8963 . . . . 5 ((𝑓 ∈ V ∧ ran 𝑓 ∈ V ∧ 𝑓:𝐴–1-1β†’ran 𝑓) β†’ 𝐴 β‰Ό ran 𝑓)
114, 5, 9, 10mp3an12i 1466 . . . 4 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ 𝐴 β‰Ό ran 𝑓)
12 sdomnen 8977 . . . . . . . 8 (𝐴 β‰Ί 𝐡 β†’ Β¬ 𝐴 β‰ˆ 𝐡)
1312adantr 482 . . . . . . 7 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ Β¬ 𝐴 β‰ˆ 𝐡)
14 ssdif0 4364 . . . . . . . 8 (𝐡 βŠ† ran 𝑓 ↔ (𝐡 βˆ– ran 𝑓) = βˆ…)
15 simplr 768 . . . . . . . . . . 11 (((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) ∧ 𝐡 βŠ† ran 𝑓) β†’ 𝑓:𝐴–1-1→𝐡)
16 f1f 6788 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1→𝐡 β†’ 𝑓:𝐴⟢𝐡)
1716frnd 6726 . . . . . . . . . . . . 13 (𝑓:𝐴–1-1→𝐡 β†’ ran 𝑓 βŠ† 𝐡)
1815, 17syl 17 . . . . . . . . . . . 12 (((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) ∧ 𝐡 βŠ† ran 𝑓) β†’ ran 𝑓 βŠ† 𝐡)
19 simpr 486 . . . . . . . . . . . 12 (((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) ∧ 𝐡 βŠ† ran 𝑓) β†’ 𝐡 βŠ† ran 𝑓)
2018, 19eqssd 4000 . . . . . . . . . . 11 (((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) ∧ 𝐡 βŠ† ran 𝑓) β†’ ran 𝑓 = 𝐡)
21 dff1o5 6843 . . . . . . . . . . 11 (𝑓:𝐴–1-1-onto→𝐡 ↔ (𝑓:𝐴–1-1→𝐡 ∧ ran 𝑓 = 𝐡))
2215, 20, 21sylanbrc 584 . . . . . . . . . 10 (((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) ∧ 𝐡 βŠ† ran 𝑓) β†’ 𝑓:𝐴–1-1-onto→𝐡)
23 f1oen3g 8962 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:𝐴–1-1-onto→𝐡) β†’ 𝐴 β‰ˆ 𝐡)
244, 22, 23sylancr 588 . . . . . . . . 9 (((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) ∧ 𝐡 βŠ† ran 𝑓) β†’ 𝐴 β‰ˆ 𝐡)
2524ex 414 . . . . . . . 8 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ (𝐡 βŠ† ran 𝑓 β†’ 𝐴 β‰ˆ 𝐡))
2614, 25biimtrrid 242 . . . . . . 7 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ ((𝐡 βˆ– ran 𝑓) = βˆ… β†’ 𝐴 β‰ˆ 𝐡))
2713, 26mtod 197 . . . . . 6 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ Β¬ (𝐡 βˆ– ran 𝑓) = βˆ…)
28 neq0 4346 . . . . . 6 (Β¬ (𝐡 βˆ– ran 𝑓) = βˆ… ↔ βˆƒπ‘€ 𝑀 ∈ (𝐡 βˆ– ran 𝑓))
2927, 28sylib 217 . . . . 5 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ βˆƒπ‘€ 𝑀 ∈ (𝐡 βˆ– ran 𝑓))
30 snssi 4812 . . . . . . 7 (𝑀 ∈ (𝐡 βˆ– ran 𝑓) β†’ {𝑀} βŠ† (𝐡 βˆ– ran 𝑓))
31 relsdom 8946 . . . . . . . . . . 11 Rel β‰Ί
3231brrelex1i 5733 . . . . . . . . . 10 (𝐴 β‰Ί 𝐡 β†’ 𝐴 ∈ V)
3332adantr 482 . . . . . . . . 9 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ 𝐴 ∈ V)
34 vex 3479 . . . . . . . . 9 𝑀 ∈ V
35 en2sn 9041 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝑀 ∈ V) β†’ {𝐴} β‰ˆ {𝑀})
3633, 34, 35sylancl 587 . . . . . . . 8 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ {𝐴} β‰ˆ {𝑀})
3731brrelex2i 5734 . . . . . . . . . 10 (𝐴 β‰Ί 𝐡 β†’ 𝐡 ∈ V)
3837adantr 482 . . . . . . . . 9 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ 𝐡 ∈ V)
39 difexg 5328 . . . . . . . . 9 (𝐡 ∈ V β†’ (𝐡 βˆ– ran 𝑓) ∈ V)
40 snfi 9044 . . . . . . . . . . 11 {𝑀} ∈ Fin
41 ssdomfi2 9200 . . . . . . . . . . 11 (({𝑀} ∈ Fin ∧ (𝐡 βˆ– ran 𝑓) ∈ V ∧ {𝑀} βŠ† (𝐡 βˆ– ran 𝑓)) β†’ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓))
4240, 41mp3an1 1449 . . . . . . . . . 10 (((𝐡 βˆ– ran 𝑓) ∈ V ∧ {𝑀} βŠ† (𝐡 βˆ– ran 𝑓)) β†’ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓))
4342ex 414 . . . . . . . . 9 ((𝐡 βˆ– ran 𝑓) ∈ V β†’ ({𝑀} βŠ† (𝐡 βˆ– ran 𝑓) β†’ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓)))
4438, 39, 433syl 18 . . . . . . . 8 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ ({𝑀} βŠ† (𝐡 βˆ– ran 𝑓) β†’ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓)))
45 endom 8975 . . . . . . . . 9 ({𝐴} β‰ˆ {𝑀} β†’ {𝐴} β‰Ό {𝑀})
46 domtrfi 9196 . . . . . . . . . 10 (({𝑀} ∈ Fin ∧ {𝐴} β‰Ό {𝑀} ∧ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓)) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓))
4740, 46mp3an1 1449 . . . . . . . . 9 (({𝐴} β‰Ό {𝑀} ∧ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓)) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓))
4845, 47sylan 581 . . . . . . . 8 (({𝐴} β‰ˆ {𝑀} ∧ {𝑀} β‰Ό (𝐡 βˆ– ran 𝑓)) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓))
4936, 44, 48syl6an 683 . . . . . . 7 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ ({𝑀} βŠ† (𝐡 βˆ– ran 𝑓) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓)))
5030, 49syl5 34 . . . . . 6 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ (𝑀 ∈ (𝐡 βˆ– ran 𝑓) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓)))
5150exlimdv 1937 . . . . 5 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ (βˆƒπ‘€ 𝑀 ∈ (𝐡 βˆ– ran 𝑓) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓)))
5229, 51mpd 15 . . . 4 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓))
53 disjdif 4472 . . . . 5 (ran 𝑓 ∩ (𝐡 βˆ– ran 𝑓)) = βˆ…
5453a1i 11 . . . 4 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ (ran 𝑓 ∩ (𝐡 βˆ– ran 𝑓)) = βˆ…)
55 undom 9059 . . . 4 (((𝐴 β‰Ό ran 𝑓 ∧ {𝐴} β‰Ό (𝐡 βˆ– ran 𝑓)) ∧ (ran 𝑓 ∩ (𝐡 βˆ– ran 𝑓)) = βˆ…) β†’ (𝐴 βˆͺ {𝐴}) β‰Ό (ran 𝑓 βˆͺ (𝐡 βˆ– ran 𝑓)))
5611, 52, 54, 55syl21anc 837 . . 3 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ (𝐴 βˆͺ {𝐴}) β‰Ό (ran 𝑓 βˆͺ (𝐡 βˆ– ran 𝑓)))
57 df-suc 6371 . . . 4 suc 𝐴 = (𝐴 βˆͺ {𝐴})
5857a1i 11 . . 3 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ suc 𝐴 = (𝐴 βˆͺ {𝐴}))
59 undif2 4477 . . . 4 (ran 𝑓 βˆͺ (𝐡 βˆ– ran 𝑓)) = (ran 𝑓 βˆͺ 𝐡)
6017adantl 483 . . . . 5 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ ran 𝑓 βŠ† 𝐡)
61 ssequn1 4181 . . . . 5 (ran 𝑓 βŠ† 𝐡 ↔ (ran 𝑓 βˆͺ 𝐡) = 𝐡)
6260, 61sylib 217 . . . 4 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ (ran 𝑓 βˆͺ 𝐡) = 𝐡)
6359, 62eqtr2id 2786 . . 3 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ 𝐡 = (ran 𝑓 βˆͺ (𝐡 βˆ– ran 𝑓)))
6456, 58, 633brtr4d 5181 . 2 ((𝐴 β‰Ί 𝐡 ∧ 𝑓:𝐴–1-1→𝐡) β†’ suc 𝐴 β‰Ό 𝐡)
653, 64exlimddv 1939 1 (𝐴 β‰Ί 𝐡 β†’ suc 𝐴 β‰Ό 𝐡)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  {csn 4629   class class class wbr 5149  ran crn 5678  suc csuc 6367  β€“1-1β†’wf1 6541  β€“1-1-ontoβ†’wf1o 6543   β‰ˆ cen 8936   β‰Ό cdom 8937   β‰Ί csdm 8938  Fincfn 8939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7856  df-1o 8466  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943
This theorem is referenced by:  sucdom  9235  sucdomOLD  9236  card2inf  9550
  Copyright terms: Public domain W3C validator