Metamath Proof Explorer

Theorem lfuhgr1v0e

Description: A loop-free hypergraph with one vertex has no edges. (Contributed by AV, 18-Oct-2020) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypotheses lfuhgr1v0e.v ⊢V=Vtx⁡G
lfuhgr1v0e.i ⊢I=iEdg⁡G
lfuhgr1v0e.e ⊢E=x∈𝒫V|2≤x
Assertion lfuhgr1v0e ⊢G∈UHGraph∧V=1∧I:dom⁡I⟶E→Edg⁡G=∅

Proof

Step Hyp Ref Expression
1 lfuhgr1v0e.v ⊢V=Vtx⁡G
2 lfuhgr1v0e.i ⊢I=iEdg⁡G
3 lfuhgr1v0e.e ⊢E=x∈𝒫V|2≤x
4 2 a1i ⊢G∈UHGraph∧V=1→I=iEdg⁡G
5 2 dmeqi ⊢dom⁡I=dom⁡iEdg⁡G
6 5 a1i ⊢G∈UHGraph∧V=1→dom⁡I=dom⁡iEdg⁡G
7 1 fvexi ⊢V∈V
8 hash1snb ⊢V∈V→V=1↔∃vV=v
9 7 8 ax-mp ⊢V=1↔∃vV=v
10 pweq ⊢V=v→𝒫V=𝒫v
11 10 rabeqdv ⊢V=v→x∈𝒫V|2≤x=x∈𝒫v|2≤x
12 2pos ⊢0<2
13 0re ⊢0∈ℝ
14 2re ⊢2∈ℝ
15 13 14 ltnlei ⊢0<2↔¬2≤0
16 12 15 mpbi ⊢¬2≤0
17 1lt2 ⊢1<2
18 1re ⊢1∈ℝ
19 18 14 ltnlei ⊢1<2↔¬2≤1
20 17 19 mpbi ⊢¬2≤1
21 0ex ⊢∅∈V
22 vsnex ⊢v∈V
23 fveq2 ⊢x=∅→x=∅
24 hash0 ⊢∅=0
25 23 24 eqtrdi ⊢x=∅→x=0
26 25 breq2d ⊢x=∅→2≤x↔2≤0
27 26 notbid ⊢x=∅→¬2≤x↔¬2≤0
28 fveq2 ⊢x=v→x=v
29 hashsng ⊢v∈V→v=1
30 29 elv ⊢v=1
31 28 30 eqtrdi ⊢x=v→x=1
32 31 breq2d ⊢x=v→2≤x↔2≤1
33 32 notbid ⊢x=v→¬2≤x↔¬2≤1
34 21 22 27 33 ralpr ⊢∀x∈∅v¬2≤x↔¬2≤0∧¬2≤1
35 16 20 34 mpbir2an ⊢∀x∈∅v¬2≤x
36 pwsn ⊢𝒫v=∅v
37 36 raleqi ⊢∀x∈𝒫v¬2≤x↔∀x∈∅v¬2≤x
38 35 37 mpbir ⊢∀x∈𝒫v¬2≤x
39 rabeq0 ⊢x∈𝒫v|2≤x=∅↔∀x∈𝒫v¬2≤x
40 38 39 mpbir ⊢x∈𝒫v|2≤x=∅
41 11 40 eqtrdi ⊢V=v→x∈𝒫V|2≤x=∅
42 41 a1d ⊢V=v→G∈UHGraph→x∈𝒫V|2≤x=∅
43 42 exlimiv ⊢∃vV=v→G∈UHGraph→x∈𝒫V|2≤x=∅
44 9 43 sylbi ⊢V=1→G∈UHGraph→x∈𝒫V|2≤x=∅
45 44 impcom ⊢G∈UHGraph∧V=1→x∈𝒫V|2≤x=∅
46 3 45 eqtrid ⊢G∈UHGraph∧V=1→E=∅
47 4 6 46 feq123d ⊢G∈UHGraph∧V=1→I:dom⁡I⟶E↔iEdg⁡G:dom⁡iEdg⁡G⟶∅
48 47 biimp3a ⊢G∈UHGraph∧V=1∧I:dom⁡I⟶E→iEdg⁡G:dom⁡iEdg⁡G⟶∅
49 f00 ⊢iEdg⁡G:dom⁡iEdg⁡G⟶∅↔iEdg⁡G=∅∧dom⁡iEdg⁡G=∅
50 49 simplbi ⊢iEdg⁡G:dom⁡iEdg⁡G⟶∅→iEdg⁡G=∅
51 48 50 syl ⊢G∈UHGraph∧V=1∧I:dom⁡I⟶E→iEdg⁡G=∅
52 uhgriedg0edg0 ⊢G∈UHGraph→Edg⁡G=∅↔iEdg⁡G=∅
53 52 3ad2ant1 ⊢G∈UHGraph∧V=1∧I:dom⁡I⟶E→Edg⁡G=∅↔iEdg⁡G=∅
54 51 53 mpbird ⊢G∈UHGraph∧V=1∧I:dom⁡I⟶E→Edg⁡G=∅