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 = ∅