Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  unidifsnne Structured version   Visualization version   GIF version

Theorem unidifsnne 32464
Description: The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017.)
Assertion
Ref Expression
unidifsnne ((𝑋𝑃𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ≠ 𝑋)

Proof of Theorem unidifsnne
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 2onn 8674 . . . . . . . . . 10 2o ∈ ω
2 nnfi 9207 . . . . . . . . . 10 (2o ∈ ω → 2o ∈ Fin)
31, 2ax-mp 5 . . . . . . . . 9 2o ∈ Fin
4 enfi 9226 . . . . . . . . 9 (𝑃 ≈ 2o → (𝑃 ∈ Fin ↔ 2o ∈ Fin))
53, 4mpbiri 257 . . . . . . . 8 (𝑃 ≈ 2o𝑃 ∈ Fin)
65adantl 480 . . . . . . 7 ((𝑋𝑃𝑃 ≈ 2o) → 𝑃 ∈ Fin)
7 diffi 9215 . . . . . . 7 (𝑃 ∈ Fin → (𝑃 ∖ {𝑋}) ∈ Fin)
86, 7syl 17 . . . . . 6 ((𝑋𝑃𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ∈ Fin)
98cardidd 10594 . . . . 5 ((𝑋𝑃𝑃 ≈ 2o) → (card‘(𝑃 ∖ {𝑋})) ≈ (𝑃 ∖ {𝑋}))
109ensymd 9038 . . . 4 ((𝑋𝑃𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ≈ (card‘(𝑃 ∖ {𝑋})))
11 simpl 481 . . . . . . 7 ((𝑋𝑃𝑃 ≈ 2o) → 𝑋𝑃)
12 dif1card 10055 . . . . . . 7 ((𝑃 ∈ Fin ∧ 𝑋𝑃) → (card‘𝑃) = suc (card‘(𝑃 ∖ {𝑋})))
136, 11, 12syl2anc 582 . . . . . 6 ((𝑋𝑃𝑃 ≈ 2o) → (card‘𝑃) = suc (card‘(𝑃 ∖ {𝑋})))
14 cardennn 10028 . . . . . . . . 9 ((𝑃 ≈ 2o ∧ 2o ∈ ω) → (card‘𝑃) = 2o)
151, 14mpan2 689 . . . . . . . 8 (𝑃 ≈ 2o → (card‘𝑃) = 2o)
16 df-2o 8499 . . . . . . . 8 2o = suc 1o
1715, 16eqtrdi 2782 . . . . . . 7 (𝑃 ≈ 2o → (card‘𝑃) = suc 1o)
1817adantl 480 . . . . . 6 ((𝑋𝑃𝑃 ≈ 2o) → (card‘𝑃) = suc 1o)
1913, 18eqtr3d 2768 . . . . 5 ((𝑋𝑃𝑃 ≈ 2o) → suc (card‘(𝑃 ∖ {𝑋})) = suc 1o)
20 suc11reg 9664 . . . . 5 (suc (card‘(𝑃 ∖ {𝑋})) = suc 1o ↔ (card‘(𝑃 ∖ {𝑋})) = 1o)
2119, 20sylib 217 . . . 4 ((𝑋𝑃𝑃 ≈ 2o) → (card‘(𝑃 ∖ {𝑋})) = 1o)
2210, 21breqtrd 5181 . . 3 ((𝑋𝑃𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ≈ 1o)
23 en1 9059 . . 3 ((𝑃 ∖ {𝑋}) ≈ 1o ↔ ∃𝑥(𝑃 ∖ {𝑋}) = {𝑥})
2422, 23sylib 217 . 2 ((𝑋𝑃𝑃 ≈ 2o) → ∃𝑥(𝑃 ∖ {𝑋}) = {𝑥})
25 simplll 773 . . . . . . 7 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → 𝑋𝑃)
2625elexd 3485 . . . . . 6 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → 𝑋 ∈ V)
27 simplr 767 . . . . . . . . . . 11 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → (𝑃 ∖ {𝑋}) = {𝑥})
28 sneqbg 4852 . . . . . . . . . . . . 13 (𝑋𝑃 → ({𝑋} = {𝑥} ↔ 𝑋 = 𝑥))
2928biimpar 476 . . . . . . . . . . . 12 ((𝑋𝑃𝑋 = 𝑥) → {𝑋} = {𝑥})
3029ad4ant14 750 . . . . . . . . . . 11 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → {𝑋} = {𝑥})
3127, 30eqtr4d 2769 . . . . . . . . . 10 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → (𝑃 ∖ {𝑋}) = {𝑋})
3231ineq2d 4213 . . . . . . . . 9 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → ({𝑋} ∩ (𝑃 ∖ {𝑋})) = ({𝑋} ∩ {𝑋}))
33 disjdif 4476 . . . . . . . . 9 ({𝑋} ∩ (𝑃 ∖ {𝑋})) = ∅
34 inidm 4220 . . . . . . . . 9 ({𝑋} ∩ {𝑋}) = {𝑋}
3532, 33, 343eqtr3g 2789 . . . . . . . 8 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → ∅ = {𝑋})
3635eqcomd 2732 . . . . . . 7 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → {𝑋} = ∅)
37 snprc 4726 . . . . . . 7 𝑋 ∈ V ↔ {𝑋} = ∅)
3836, 37sylibr 233 . . . . . 6 ((((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → ¬ 𝑋 ∈ V)
3926, 38pm2.65da 815 . . . . 5 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → ¬ 𝑋 = 𝑥)
4039neqned 2937 . . . 4 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → 𝑋𝑥)
41 simpr 483 . . . . . 6 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → (𝑃 ∖ {𝑋}) = {𝑥})
4241unieqd 4928 . . . . 5 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → (𝑃 ∖ {𝑋}) = {𝑥})
43 unisnv 4937 . . . . 5 {𝑥} = 𝑥
4442, 43eqtrdi 2782 . . . 4 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → (𝑃 ∖ {𝑋}) = 𝑥)
4540, 44neeqtrrd 3005 . . 3 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → 𝑋 (𝑃 ∖ {𝑋}))
4645necomd 2986 . 2 (((𝑋𝑃𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → (𝑃 ∖ {𝑋}) ≠ 𝑋)
4724, 46exlimddv 1931 1 ((𝑋𝑃𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ≠ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1534  wex 1774  wcel 2099  wne 2930  Vcvv 3462  cdif 3944  cin 3946  c0 4325  {csn 4633   cuni 4915   class class class wbr 5155  suc csuc 6380  cfv 6556  ωcom 7878  1oc1o 8491  2oc2o 8492  cen 8973  Fincfn 8976  cardccrd 9980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5292  ax-sep 5306  ax-nul 5313  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-reg 9637  ax-ac2 10508
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-int 4957  df-iun 5005  df-br 5156  df-opab 5218  df-mpt 5239  df-tr 5273  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-se 5640  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6314  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-isom 6565  df-riota 7382  df-ov 7429  df-om 7879  df-2nd 8006  df-frecs 8298  df-wrecs 8329  df-recs 8403  df-1o 8498  df-2o 8499  df-er 8736  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-card 9984  df-ac 10161
This theorem is referenced by:  cyc3genpmlem  33031
  Copyright terms: Public domain W3C validator