Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lfuhgr1v0e Structured version   Visualization version   GIF version

Theorem lfuhgr1v0e 40482
Description: A loop-free hypergraph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 2-Apr-2021.)
Hypotheses
Ref Expression
lfuhgr1v0e.v 𝑉 = (Vtx‘𝐺)
lfuhgr1v0e.i 𝐼 = (iEdg‘𝐺)
lfuhgr1v0e.e 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)}
Assertion
Ref Expression
lfuhgr1v0e ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1 ∧ 𝐼:dom 𝐼𝐸) → (Edg‘𝐺) = ∅)
Distinct variable groups:   𝑥,𝐺   𝑥,𝑉
Allowed substitution hints:   𝐸(𝑥)   𝐼(𝑥)

Proof of Theorem lfuhgr1v0e
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 lfuhgr1v0e.i . . . . . 6 𝐼 = (iEdg‘𝐺)
21a1i 11 . . . . 5 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1) → 𝐼 = (iEdg‘𝐺))
31dmeqi 5234 . . . . . 6 dom 𝐼 = dom (iEdg‘𝐺)
43a1i 11 . . . . 5 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1) → dom 𝐼 = dom (iEdg‘𝐺))
5 lfuhgr1v0e.e . . . . . 6 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)}
6 lfuhgr1v0e.v . . . . . . . . . 10 𝑉 = (Vtx‘𝐺)
7 fvex 6098 . . . . . . . . . 10 (Vtx‘𝐺) ∈ V
86, 7eqeltri 2683 . . . . . . . . 9 𝑉 ∈ V
9 hash1snb 13020 . . . . . . . . 9 (𝑉 ∈ V → ((#‘𝑉) = 1 ↔ ∃𝑣 𝑉 = {𝑣}))
108, 9ax-mp 5 . . . . . . . 8 ((#‘𝑉) = 1 ↔ ∃𝑣 𝑉 = {𝑣})
11 pweq 4110 . . . . . . . . . . . 12 (𝑉 = {𝑣} → 𝒫 𝑉 = 𝒫 {𝑣})
1211rabeqdv 3166 . . . . . . . . . . 11 (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (#‘𝑥)})
13 2pos 10959 . . . . . . . . . . . . . . 15 0 < 2
14 0re 9896 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
15 2re 10937 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
1614, 15ltnlei 10009 . . . . . . . . . . . . . . 15 (0 < 2 ↔ ¬ 2 ≤ 0)
1713, 16mpbi 218 . . . . . . . . . . . . . 14 ¬ 2 ≤ 0
18 1lt2 11041 . . . . . . . . . . . . . . 15 1 < 2
19 1re 9895 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
2019, 15ltnlei 10009 . . . . . . . . . . . . . . 15 (1 < 2 ↔ ¬ 2 ≤ 1)
2118, 20mpbi 218 . . . . . . . . . . . . . 14 ¬ 2 ≤ 1
22 0ex 4713 . . . . . . . . . . . . . . 15 ∅ ∈ V
23 snex 4830 . . . . . . . . . . . . . . 15 {𝑣} ∈ V
24 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
25 hash0 12971 . . . . . . . . . . . . . . . . . 18 (#‘∅) = 0
2624, 25syl6eq 2659 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (#‘𝑥) = 0)
2726breq2d 4589 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (2 ≤ (#‘𝑥) ↔ 2 ≤ 0))
2827notbid 306 . . . . . . . . . . . . . . 15 (𝑥 = ∅ → (¬ 2 ≤ (#‘𝑥) ↔ ¬ 2 ≤ 0))
29 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑥 = {𝑣} → (#‘𝑥) = (#‘{𝑣}))
30 vex 3175 . . . . . . . . . . . . . . . . . . 19 𝑣 ∈ V
31 hashsng 12972 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ V → (#‘{𝑣}) = 1)
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . 18 (#‘{𝑣}) = 1
3329, 32syl6eq 2659 . . . . . . . . . . . . . . . . 17 (𝑥 = {𝑣} → (#‘𝑥) = 1)
3433breq2d 4589 . . . . . . . . . . . . . . . 16 (𝑥 = {𝑣} → (2 ≤ (#‘𝑥) ↔ 2 ≤ 1))
3534notbid 306 . . . . . . . . . . . . . . 15 (𝑥 = {𝑣} → (¬ 2 ≤ (#‘𝑥) ↔ ¬ 2 ≤ 1))
3622, 23, 28, 35ralpr 4184 . . . . . . . . . . . . . 14 (∀𝑥 ∈ {∅, {𝑣}} ¬ 2 ≤ (#‘𝑥) ↔ (¬ 2 ≤ 0 ∧ ¬ 2 ≤ 1))
3717, 21, 36mpbir2an 956 . . . . . . . . . . . . 13 𝑥 ∈ {∅, {𝑣}} ¬ 2 ≤ (#‘𝑥)
38 pwsn 4360 . . . . . . . . . . . . . 14 𝒫 {𝑣} = {∅, {𝑣}}
3938raleqi 3118 . . . . . . . . . . . . 13 (∀𝑥 ∈ 𝒫 {𝑣} ¬ 2 ≤ (#‘𝑥) ↔ ∀𝑥 ∈ {∅, {𝑣}} ¬ 2 ≤ (#‘𝑥))
4037, 39mpbir 219 . . . . . . . . . . . 12 𝑥 ∈ 𝒫 {𝑣} ¬ 2 ≤ (#‘𝑥)
41 rabeq0 3910 . . . . . . . . . . . 12 ({𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (#‘𝑥)} = ∅ ↔ ∀𝑥 ∈ 𝒫 {𝑣} ¬ 2 ≤ (#‘𝑥))
4240, 41mpbir 219 . . . . . . . . . . 11 {𝑥 ∈ 𝒫 {𝑣} ∣ 2 ≤ (#‘𝑥)} = ∅
4312, 42syl6eq 2659 . . . . . . . . . 10 (𝑉 = {𝑣} → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅)
4443a1d 25 . . . . . . . . 9 (𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅))
4544exlimiv 1844 . . . . . . . 8 (∃𝑣 𝑉 = {𝑣} → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅))
4610, 45sylbi 205 . . . . . . 7 ((#‘𝑉) = 1 → (𝐺 ∈ UHGraph → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅))
4746impcom 444 . . . . . 6 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1) → {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = ∅)
485, 47syl5eq 2655 . . . . 5 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1) → 𝐸 = ∅)
492, 4, 48feq123d 5933 . . . 4 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1) → (𝐼:dom 𝐼𝐸 ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅))
5049biimp3a 1423 . . 3 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1 ∧ 𝐼:dom 𝐼𝐸) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅)
51 f00 5985 . . . 4 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅ ↔ ((iEdg‘𝐺) = ∅ ∧ dom (iEdg‘𝐺) = ∅))
5251simplbi 474 . . 3 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅ → (iEdg‘𝐺) = ∅)
5350, 52syl 17 . 2 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1 ∧ 𝐼:dom 𝐼𝐸) → (iEdg‘𝐺) = ∅)
54 uhgriedg0edg0 40362 . . 3 (𝐺 ∈ UHGraph → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅))
55543ad2ant1 1074 . 2 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1 ∧ 𝐼:dom 𝐼𝐸) → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅))
5653, 55mpbird 245 1 ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1 ∧ 𝐼:dom 𝐼𝐸) → (Edg‘𝐺) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wral 2895  {crab 2899  Vcvv 3172  c0 3873  𝒫 cpw 4107  {csn 4124  {cpr 4126   class class class wbr 4577  dom cdm 5028  wf 5786  cfv 5790  0cc0 9792  1c1 9793   < clt 9930  cle 9931  2c2 10917  #chash 12934  Vtxcvtx 40231  iEdgciedg 40232   UHGraph cuhgr 40280  Edgcedga 40353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-n0 11140  df-z 11211  df-uz 11520  df-fz 12153  df-hash 12935  df-uhgr 40282  df-edga 40354
This theorem is referenced by:  usgr1vr  40483  vtxdlfuhgr1v  40696
  Copyright terms: Public domain W3C validator