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

Theorem cusgrfilem3 26559
 Description: Lemma 3 for cusgrfi 26560. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
Hypotheses
Ref Expression
cusgrfi.v 𝑉 = (Vtx‘𝐺)
cusgrfi.p 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎𝑉 (𝑎𝑁𝑥 = {𝑎, 𝑁})}
cusgrfi.f 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})
Assertion
Ref Expression
cusgrfilem3 (𝑁𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin))
Distinct variable groups:   𝑥,𝐺   𝑁,𝑎,𝑥   𝑉,𝑎,𝑥   𝑥,𝑃
Allowed substitution hints:   𝑃(𝑎)   𝐹(𝑥,𝑎)   𝐺(𝑎)

Proof of Theorem cusgrfilem3
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 diffi 8353 . . 3 (𝑉 ∈ Fin → (𝑉 ∖ {𝑁}) ∈ Fin)
2 simpr 479 . . . . . 6 ((𝑁𝑉 ∧ ¬ 𝑉 ∈ Fin) → ¬ 𝑉 ∈ Fin)
3 snfi 8199 . . . . . 6 {𝑁} ∈ Fin
4 difinf 8391 . . . . . 6 ((¬ 𝑉 ∈ Fin ∧ {𝑁} ∈ Fin) → ¬ (𝑉 ∖ {𝑁}) ∈ Fin)
52, 3, 4sylancl 697 . . . . 5 ((𝑁𝑉 ∧ ¬ 𝑉 ∈ Fin) → ¬ (𝑉 ∖ {𝑁}) ∈ Fin)
65ex 449 . . . 4 (𝑁𝑉 → (¬ 𝑉 ∈ Fin → ¬ (𝑉 ∖ {𝑁}) ∈ Fin))
76con4d 114 . . 3 (𝑁𝑉 → ((𝑉 ∖ {𝑁}) ∈ Fin → 𝑉 ∈ Fin))
81, 7impbid2 216 . 2 (𝑁𝑉 → (𝑉 ∈ Fin ↔ (𝑉 ∖ {𝑁}) ∈ Fin))
9 cusgrfi.f . . . . . 6 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})
10 cusgrfi.v . . . . . . . . 9 𝑉 = (Vtx‘𝐺)
11 fvex 6358 . . . . . . . . 9 (Vtx‘𝐺) ∈ V
1210, 11eqeltri 2831 . . . . . . . 8 𝑉 ∈ V
13 difexg 4956 . . . . . . . 8 (𝑉 ∈ V → (𝑉 ∖ {𝑁}) ∈ V)
1412, 13ax-mp 5 . . . . . . 7 (𝑉 ∖ {𝑁}) ∈ V
15 mptexg 6644 . . . . . . 7 ((𝑉 ∖ {𝑁}) ∈ V → (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ∈ V)
1614, 15mp1i 13 . . . . . 6 (𝑁𝑉 → (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ∈ V)
179, 16syl5eqel 2839 . . . . 5 (𝑁𝑉𝐹 ∈ V)
18 cusgrfi.p . . . . . 6 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎𝑉 (𝑎𝑁𝑥 = {𝑎, 𝑁})}
1910, 18, 9cusgrfilem2 26558 . . . . 5 (𝑁𝑉𝐹:(𝑉 ∖ {𝑁})–1-1-onto𝑃)
20 f1oeq1 6284 . . . . . 6 (𝑓 = 𝐹 → (𝑓:(𝑉 ∖ {𝑁})–1-1-onto𝑃𝐹:(𝑉 ∖ {𝑁})–1-1-onto𝑃))
2120spcegv 3430 . . . . 5 (𝐹 ∈ V → (𝐹:(𝑉 ∖ {𝑁})–1-1-onto𝑃 → ∃𝑓 𝑓:(𝑉 ∖ {𝑁})–1-1-onto𝑃))
2217, 19, 21sylc 65 . . . 4 (𝑁𝑉 → ∃𝑓 𝑓:(𝑉 ∖ {𝑁})–1-1-onto𝑃)
23 bren 8126 . . . 4 ((𝑉 ∖ {𝑁}) ≈ 𝑃 ↔ ∃𝑓 𝑓:(𝑉 ∖ {𝑁})–1-1-onto𝑃)
2422, 23sylibr 224 . . 3 (𝑁𝑉 → (𝑉 ∖ {𝑁}) ≈ 𝑃)
25 enfi 8337 . . 3 ((𝑉 ∖ {𝑁}) ≈ 𝑃 → ((𝑉 ∖ {𝑁}) ∈ Fin ↔ 𝑃 ∈ Fin))
2624, 25syl 17 . 2 (𝑁𝑉 → ((𝑉 ∖ {𝑁}) ∈ Fin ↔ 𝑃 ∈ Fin))
278, 26bitrd 268 1 (𝑁𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1628  ∃wex 1849   ∈ wcel 2135   ≠ wne 2928  ∃wrex 3047  {crab 3050  Vcvv 3336   ∖ cdif 3708  𝒫 cpw 4298  {csn 4317  {cpr 4319   class class class wbr 4800   ↦ cmpt 4877  –1-1-onto→wf1o 6044  ‘cfv 6045   ≈ cen 8114  Fincfn 8117  Vtxcvtx 26069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-en 8118  df-fin 8121 This theorem is referenced by:  cusgrfi  26560
 Copyright terms: Public domain W3C validator