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

Theorem isprm2lem 15321
Description: Lemma for isprm2 15322. (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
isprm2lem ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛𝑃} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} = {1, 𝑃}))
Distinct variable group:   𝑃,𝑛

Proof of Theorem isprm2lem
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 neeq1 2852 . . . 4 (𝑝 = 𝑃 → (𝑝 ≠ 1 ↔ 𝑃 ≠ 1))
2 breq2 4619 . . . . . . 7 (𝑝 = 𝑃 → (𝑛𝑝𝑛𝑃))
32rabbidv 3177 . . . . . 6 (𝑝 = 𝑃 → {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑃})
43breq1d 4625 . . . . 5 (𝑝 = 𝑃 → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} ≈ 2𝑜))
5 preq2 4241 . . . . . 6 (𝑝 = 𝑃 → {1, 𝑝} = {1, 𝑃})
63, 5eqeq12d 2636 . . . . 5 (𝑝 = 𝑃 → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝} ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} = {1, 𝑃}))
74, 6bibi12d 335 . . . 4 (𝑝 = 𝑃 → (({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝}) ↔ ({𝑛 ∈ ℕ ∣ 𝑛𝑃} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} = {1, 𝑃})))
81, 7imbi12d 334 . . 3 (𝑝 = 𝑃 → ((𝑝 ≠ 1 → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝})) ↔ (𝑃 ≠ 1 → ({𝑛 ∈ ℕ ∣ 𝑛𝑃} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} = {1, 𝑃}))))
9 1idssfct 15320 . . . . . . . 8 (𝑝 ∈ ℕ → {1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝})
10 disjsn 4218 . . . . . . . . . . . 12 (({1} ∩ {𝑝}) = ∅ ↔ ¬ 𝑝 ∈ {1})
11 1ex 9982 . . . . . . . . . . . . . 14 1 ∈ V
1211ensn1 7967 . . . . . . . . . . . . 13 {1} ≈ 1𝑜
13 vex 3189 . . . . . . . . . . . . . 14 𝑝 ∈ V
1413ensn1 7967 . . . . . . . . . . . . 13 {𝑝} ≈ 1𝑜
15 pm54.43 8773 . . . . . . . . . . . . 13 (({1} ≈ 1𝑜 ∧ {𝑝} ≈ 1𝑜) → (({1} ∩ {𝑝}) = ∅ ↔ ({1} ∪ {𝑝}) ≈ 2𝑜))
1612, 14, 15mp2an 707 . . . . . . . . . . . 12 (({1} ∩ {𝑝}) = ∅ ↔ ({1} ∪ {𝑝}) ≈ 2𝑜)
1710, 16bitr3i 266 . . . . . . . . . . 11 𝑝 ∈ {1} ↔ ({1} ∪ {𝑝}) ≈ 2𝑜)
18 velsn 4166 . . . . . . . . . . 11 (𝑝 ∈ {1} ↔ 𝑝 = 1)
1917, 18xchnxbi 322 . . . . . . . . . 10 𝑝 = 1 ↔ ({1} ∪ {𝑝}) ≈ 2𝑜)
20 df-ne 2791 . . . . . . . . . 10 (𝑝 ≠ 1 ↔ ¬ 𝑝 = 1)
21 df-pr 4153 . . . . . . . . . . 11 {1, 𝑝} = ({1} ∪ {𝑝})
2221breq1i 4622 . . . . . . . . . 10 ({1, 𝑝} ≈ 2𝑜 ↔ ({1} ∪ {𝑝}) ≈ 2𝑜)
2319, 20, 223bitr4i 292 . . . . . . . . 9 (𝑝 ≠ 1 ↔ {1, 𝑝} ≈ 2𝑜)
24 ensym 7952 . . . . . . . . . 10 ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 → 2𝑜 ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝})
25 entr 7955 . . . . . . . . . 10 (({1, 𝑝} ≈ 2𝑜 ∧ 2𝑜 ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝})
2624, 25sylan2 491 . . . . . . . . 9 (({1, 𝑝} ≈ 2𝑜 ∧ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜) → {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝})
2723, 26sylanb 489 . . . . . . . 8 ((𝑝 ≠ 1 ∧ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜) → {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝})
28 prfi 8182 . . . . . . . . . . 11 {1, 𝑝} ∈ Fin
29 ensym 7952 . . . . . . . . . . 11 ({1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝} → {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ {1, 𝑝})
30 enfii 8124 . . . . . . . . . . 11 (({1, 𝑝} ∈ Fin ∧ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ {1, 𝑝}) → {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin)
3128, 29, 30sylancr 694 . . . . . . . . . 10 ({1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝} → {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin)
3231adantl 482 . . . . . . . . 9 (({1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin)
33 dfpss2 3672 . . . . . . . . . . . 12 ({1, 𝑝} ⊊ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ↔ ({1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ ¬ {1, 𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑝}))
34 pssinf 8117 . . . . . . . . . . . 12 (({1, 𝑝} ⊊ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → ¬ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin)
3533, 34sylanbr 490 . . . . . . . . . . 11 ((({1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ ¬ {1, 𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑝}) ∧ {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → ¬ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin)
3635an32s 845 . . . . . . . . . 10 ((({1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) ∧ ¬ {1, 𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → ¬ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin)
3736ex 450 . . . . . . . . 9 (({1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → (¬ {1, 𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑝} → ¬ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∈ Fin))
3832, 37mt4d 152 . . . . . . . 8 (({1, 𝑝} ⊆ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ∧ {1, 𝑝} ≈ {𝑛 ∈ ℕ ∣ 𝑛𝑝}) → {1, 𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑝})
399, 27, 38syl2an 494 . . . . . . 7 ((𝑝 ∈ ℕ ∧ (𝑝 ≠ 1 ∧ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜)) → {1, 𝑝} = {𝑛 ∈ ℕ ∣ 𝑛𝑝})
4039eqcomd 2627 . . . . . 6 ((𝑝 ∈ ℕ ∧ (𝑝 ≠ 1 ∧ {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜)) → {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝})
4140expr 642 . . . . 5 ((𝑝 ∈ ℕ ∧ 𝑝 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 → {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝}))
42 breq1 4618 . . . . . . . 8 ({𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝} → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 ↔ {1, 𝑝} ≈ 2𝑜))
4342, 23syl6bbr 278 . . . . . . 7 ({𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝} → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜𝑝 ≠ 1))
4443biimprcd 240 . . . . . 6 (𝑝 ≠ 1 → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝} → {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜))
4544adantl 482 . . . . 5 ((𝑝 ∈ ℕ ∧ 𝑝 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝} → {𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜))
4641, 45impbid 202 . . . 4 ((𝑝 ∈ ℕ ∧ 𝑝 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝}))
4746ex 450 . . 3 (𝑝 ∈ ℕ → (𝑝 ≠ 1 → ({𝑛 ∈ ℕ ∣ 𝑛𝑝} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑝} = {1, 𝑝})))
488, 47vtoclga 3258 . 2 (𝑃 ∈ ℕ → (𝑃 ≠ 1 → ({𝑛 ∈ ℕ ∣ 𝑛𝑃} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} = {1, 𝑃})))
4948imp 445 1 ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛𝑃} ≈ 2𝑜 ↔ {𝑛 ∈ ℕ ∣ 𝑛𝑃} = {1, 𝑃}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  {crab 2911  cun 3554  cin 3555  wss 3556  wpss 3557  c0 3893  {csn 4150  {cpr 4152   class class class wbr 4615  1𝑜c1o 7501  2𝑜c2o 7502  cen 7899  Fincfn 7902  1c1 9884  cn 10967  cdvds 14910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-z 11325  df-dvds 14911
This theorem is referenced by:  isprm2  15322
  Copyright terms: Public domain W3C validator