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 v V = v
9 7 8 ax-mp V = 1 v V = 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 snex 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 v V = 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 syl5eq 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 =