Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  dif1en GIF version

Theorem dif1en 6367
 Description: If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.)
Assertion
Ref Expression
dif1en ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)

Proof of Theorem dif1en
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 simp2 916 . . . 4 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → 𝐴 ≈ suc 𝑀)
21ensymd 6293 . . 3 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → suc 𝑀𝐴)
3 bren 6258 . . 3 (suc 𝑀𝐴 ↔ ∃𝑓 𝑓:suc 𝑀1-1-onto𝐴)
42, 3sylib 131 . 2 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → ∃𝑓 𝑓:suc 𝑀1-1-onto𝐴)
5 peano2 4345 . . . . . . . 8 (𝑀 ∈ ω → suc 𝑀 ∈ ω)
6 nnfi 6363 . . . . . . . 8 (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
75, 6syl 14 . . . . . . 7 (𝑀 ∈ ω → suc 𝑀 ∈ Fin)
873ad2ant1 936 . . . . . 6 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → suc 𝑀 ∈ Fin)
9 enfii 6365 . . . . . 6 ((suc 𝑀 ∈ Fin ∧ 𝐴 ≈ suc 𝑀) → 𝐴 ∈ Fin)
108, 1, 9syl2anc 397 . . . . 5 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → 𝐴 ∈ Fin)
1110adantr 265 . . . 4 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝐴 ∈ Fin)
12 simpl3 920 . . . 4 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑋𝐴)
13 f1of 5153 . . . . . 6 (𝑓:suc 𝑀1-1-onto𝐴𝑓:suc 𝑀𝐴)
1413adantl 266 . . . . 5 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑓:suc 𝑀𝐴)
15 sucidg 4180 . . . . . . 7 (𝑀 ∈ ω → 𝑀 ∈ suc 𝑀)
16153ad2ant1 936 . . . . . 6 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → 𝑀 ∈ suc 𝑀)
1716adantr 265 . . . . 5 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑀 ∈ suc 𝑀)
1814, 17ffvelrnd 5330 . . . 4 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓𝑀) ∈ 𝐴)
19 fidifsnen 6361 . . . 4 ((𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ (𝑓𝑀) ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ (𝐴 ∖ {(𝑓𝑀)}))
2011, 12, 18, 19syl3anc 1146 . . 3 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝐴 ∖ {𝑋}) ≈ (𝐴 ∖ {(𝑓𝑀)}))
21 nnord 4361 . . . . . . . 8 (𝑀 ∈ ω → Ord 𝑀)
22 orddif 4298 . . . . . . . 8 (Ord 𝑀𝑀 = (suc 𝑀 ∖ {𝑀}))
2321, 22syl 14 . . . . . . 7 (𝑀 ∈ ω → 𝑀 = (suc 𝑀 ∖ {𝑀}))
24233ad2ant1 936 . . . . . 6 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → 𝑀 = (suc 𝑀 ∖ {𝑀}))
2524adantr 265 . . . . 5 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑀 = (suc 𝑀 ∖ {𝑀}))
2623eleq1d 2122 . . . . . . . . 9 (𝑀 ∈ ω → (𝑀 ∈ ω ↔ (suc 𝑀 ∖ {𝑀}) ∈ ω))
2726ibi 169 . . . . . . . 8 (𝑀 ∈ ω → (suc 𝑀 ∖ {𝑀}) ∈ ω)
28273ad2ant1 936 . . . . . . 7 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → (suc 𝑀 ∖ {𝑀}) ∈ ω)
2928adantr 265 . . . . . 6 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (suc 𝑀 ∖ {𝑀}) ∈ ω)
30 dff1o2 5158 . . . . . . . . 9 (𝑓:suc 𝑀1-1-onto𝐴 ↔ (𝑓 Fn suc 𝑀 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝐴))
3130simp2bi 931 . . . . . . . 8 (𝑓:suc 𝑀1-1-onto𝐴 → Fun 𝑓)
3231adantl 266 . . . . . . 7 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → Fun 𝑓)
33 f1ofo 5160 . . . . . . . . 9 (𝑓:suc 𝑀1-1-onto𝐴𝑓:suc 𝑀onto𝐴)
3433adantl 266 . . . . . . . 8 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑓:suc 𝑀onto𝐴)
35 f1orel 5156 . . . . . . . . . . . 12 (𝑓:suc 𝑀1-1-onto𝐴 → Rel 𝑓)
3635adantl 266 . . . . . . . . . . 11 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → Rel 𝑓)
37 resdm 4676 . . . . . . . . . . 11 (Rel 𝑓 → (𝑓 ↾ dom 𝑓) = 𝑓)
3836, 37syl 14 . . . . . . . . . 10 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓 ↾ dom 𝑓) = 𝑓)
39 f1odm 5157 . . . . . . . . . . . 12 (𝑓:suc 𝑀1-1-onto𝐴 → dom 𝑓 = suc 𝑀)
4039reseq2d 4639 . . . . . . . . . . 11 (𝑓:suc 𝑀1-1-onto𝐴 → (𝑓 ↾ dom 𝑓) = (𝑓 ↾ suc 𝑀))
4140adantl 266 . . . . . . . . . 10 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓 ↾ dom 𝑓) = (𝑓 ↾ suc 𝑀))
4238, 41eqtr3d 2090 . . . . . . . . 9 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑓 = (𝑓 ↾ suc 𝑀))
43 foeq1 5129 . . . . . . . . 9 (𝑓 = (𝑓 ↾ suc 𝑀) → (𝑓:suc 𝑀onto𝐴 ↔ (𝑓 ↾ suc 𝑀):suc 𝑀onto𝐴))
4442, 43syl 14 . . . . . . . 8 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓:suc 𝑀onto𝐴 ↔ (𝑓 ↾ suc 𝑀):suc 𝑀onto𝐴))
4534, 44mpbid 139 . . . . . . 7 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓 ↾ suc 𝑀):suc 𝑀onto𝐴)
46 simpl1 918 . . . . . . . . . 10 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑀 ∈ ω)
47 f1osng 5194 . . . . . . . . . 10 ((𝑀 ∈ ω ∧ (𝑓𝑀) ∈ 𝐴) → {⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–1-1-onto→{(𝑓𝑀)})
4846, 18, 47syl2anc 397 . . . . . . . . 9 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → {⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–1-1-onto→{(𝑓𝑀)})
49 f1ofo 5160 . . . . . . . . 9 ({⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–1-1-onto→{(𝑓𝑀)} → {⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–onto→{(𝑓𝑀)})
5048, 49syl 14 . . . . . . . 8 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → {⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–onto→{(𝑓𝑀)})
51 f1ofn 5154 . . . . . . . . . . 11 (𝑓:suc 𝑀1-1-onto𝐴𝑓 Fn suc 𝑀)
5251adantl 266 . . . . . . . . . 10 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑓 Fn suc 𝑀)
53 fnressn 5376 . . . . . . . . . 10 ((𝑓 Fn suc 𝑀𝑀 ∈ suc 𝑀) → (𝑓 ↾ {𝑀}) = {⟨𝑀, (𝑓𝑀)⟩})
5452, 17, 53syl2anc 397 . . . . . . . . 9 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓 ↾ {𝑀}) = {⟨𝑀, (𝑓𝑀)⟩})
55 foeq1 5129 . . . . . . . . 9 ((𝑓 ↾ {𝑀}) = {⟨𝑀, (𝑓𝑀)⟩} → ((𝑓 ↾ {𝑀}):{𝑀}–onto→{(𝑓𝑀)} ↔ {⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–onto→{(𝑓𝑀)}))
5654, 55syl 14 . . . . . . . 8 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → ((𝑓 ↾ {𝑀}):{𝑀}–onto→{(𝑓𝑀)} ↔ {⟨𝑀, (𝑓𝑀)⟩}:{𝑀}–onto→{(𝑓𝑀)}))
5750, 56mpbird 160 . . . . . . 7 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓 ↾ {𝑀}):{𝑀}–onto→{(𝑓𝑀)})
58 resdif 5175 . . . . . . 7 ((Fun 𝑓 ∧ (𝑓 ↾ suc 𝑀):suc 𝑀onto𝐴 ∧ (𝑓 ↾ {𝑀}):{𝑀}–onto→{(𝑓𝑀)}) → (𝑓 ↾ (suc 𝑀 ∖ {𝑀})):(suc 𝑀 ∖ {𝑀})–1-1-onto→(𝐴 ∖ {(𝑓𝑀)}))
5932, 45, 57, 58syl3anc 1146 . . . . . 6 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝑓 ↾ (suc 𝑀 ∖ {𝑀})):(suc 𝑀 ∖ {𝑀})–1-1-onto→(𝐴 ∖ {(𝑓𝑀)}))
60 f1oeng 6267 . . . . . 6 (((suc 𝑀 ∖ {𝑀}) ∈ ω ∧ (𝑓 ↾ (suc 𝑀 ∖ {𝑀})):(suc 𝑀 ∖ {𝑀})–1-1-onto→(𝐴 ∖ {(𝑓𝑀)})) → (suc 𝑀 ∖ {𝑀}) ≈ (𝐴 ∖ {(𝑓𝑀)}))
6129, 59, 60syl2anc 397 . . . . 5 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (suc 𝑀 ∖ {𝑀}) ≈ (𝐴 ∖ {(𝑓𝑀)}))
6225, 61eqbrtrd 3811 . . . 4 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → 𝑀 ≈ (𝐴 ∖ {(𝑓𝑀)}))
6362ensymd 6293 . . 3 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝐴 ∖ {(𝑓𝑀)}) ≈ 𝑀)
64 entr 6294 . . 3 (((𝐴 ∖ {𝑋}) ≈ (𝐴 ∖ {(𝑓𝑀)}) ∧ (𝐴 ∖ {(𝑓𝑀)}) ≈ 𝑀) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
6520, 63, 64syl2anc 397 . 2 (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) ∧ 𝑓:suc 𝑀1-1-onto𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
664, 65exlimddv 1794 1 ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∧ w3a 896   = wceq 1259  ∃wex 1397   ∈ wcel 1409   ∖ cdif 2941  {csn 3402  ⟨cop 3405   class class class wbr 3791  Ord word 4126  suc csuc 4129  ωcom 4340  ◡ccnv 4371  dom cdm 4372  ran crn 4373   ↾ cres 4374  Rel wrel 4377  Fun wfun 4923   Fn wfn 4924  ⟶wf 4925  –onto→wfo 4927  –1-1-onto→wf1o 4928  ‘cfv 4929   ≈ cen 6249  Fincfn 6251 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338 This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-if 3359  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-er 6136  df-en 6252  df-fin 6254 This theorem is referenced by:  findcard  6375  findcard2  6376  findcard2s  6377  diffisn  6380
 Copyright terms: Public domain W3C validator