This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
lfuhgr1v0e.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
lfuhgr1v0e.e ⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
Assertion lfuhgr1v0e ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( Edg ‘ 𝐺 ) = ∅ )

Proof

Step Hyp Ref Expression
1 lfuhgr1v0e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 lfuhgr1v0e.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 lfuhgr1v0e.e ⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
4 2 a1i ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐼 = ( iEdg ‘ 𝐺 ) )
5 2 dmeqi ⊢ dom 𝐼 = dom ( iEdg ‘ 𝐺 )
6 5 a1i ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → dom 𝐼 = dom ( iEdg ‘ 𝐺 ) )
7 1 fvexi ⊢ 𝑉 ∈ V
8 hash1snb ⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
9 7 8 ax-mp ⊢ ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } )
10 pweq ⊢ ( 𝑉 = { 𝑣 } → 𝒫 𝑉 = 𝒫 { 𝑣 } )
11 10 rabeqdv ⊢ ( 𝑉 = { 𝑣 } → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ 𝒫 { 𝑣 } ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
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
23 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
24 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
25 23 24 eqtrdi ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
26 25 breq2d ⊢ ( 𝑥 = ∅ → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ 0 ) )
27 26 notbid ⊢ ( 𝑥 = ∅ → ( ¬ 2 ≤ ( ♯ ‘ 𝑥 ) ↔ ¬ 2 ≤ 0 ) )
28 fveq2 ⊢ ( 𝑥 = { 𝑣 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑣 } ) )
29 hashsng ⊢ ( 𝑣 ∈ V → ( ♯ ‘ { 𝑣 } ) = 1 )
30 29 elv ⊢ ( ♯ ‘ { 𝑣 } ) = 1
31 28 30 eqtrdi ⊢ ( 𝑥 = { 𝑣 } → ( ♯ ‘ 𝑥 ) = 1 )
32 31 breq2d ⊢ ( 𝑥 = { 𝑣 } → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ 1 ) )
33 32 notbid ⊢ ( 𝑥 = { 𝑣 } → ( ¬ 2 ≤ ( ♯ ‘ 𝑥 ) ↔ ¬ 2 ≤ 1 ) )
34 21 22 27 33 ralpr ⊢ ( ∀ 𝑥 ∈ { ∅ , { 𝑣 } } ¬ 2 ≤ ( ♯ ‘ 𝑥 ) ↔ ( ¬ 2 ≤ 0 ∧ ¬ 2 ≤ 1 ) )
35 16 20 34 mpbir2an ⊢ ∀ 𝑥 ∈ { ∅ , { 𝑣 } } ¬ 2 ≤ ( ♯ ‘ 𝑥 )
36 pwsn ⊢ 𝒫 { 𝑣 } = { ∅ , { 𝑣 } }
37 36 raleqi ⊢ ( ∀ 𝑥 ∈ 𝒫 { 𝑣 } ¬ 2 ≤ ( ♯ ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ { ∅ , { 𝑣 } } ¬ 2 ≤ ( ♯ ‘ 𝑥 ) )
38 35 37 mpbir ⊢ ∀ 𝑥 ∈ 𝒫 { 𝑣 } ¬ 2 ≤ ( ♯ ‘ 𝑥 )
39 rabeq0 ⊢ ( { 𝑥 ∈ 𝒫 { 𝑣 } ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑥 ∈ 𝒫 { 𝑣 } ¬ 2 ≤ ( ♯ ‘ 𝑥 ) )
40 38 39 mpbir ⊢ { 𝑥 ∈ 𝒫 { 𝑣 } ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅
41 11 40 eqtrdi ⊢ ( 𝑉 = { 𝑣 } → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅ )
42 41 a1d ⊢ ( 𝑉 = { 𝑣 } → ( 𝐺 ∈ UHGraph → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅ ) )
43 42 exlimiv ⊢ ( ∃ 𝑣 𝑉 = { 𝑣 } → ( 𝐺 ∈ UHGraph → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅ ) )
44 9 43 sylbi ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ( 𝐺 ∈ UHGraph → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅ ) )
45 44 impcom ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = ∅ )
46 3 45 eqtrid ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐸 = ∅ )
47 4 6 46 feq123d ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( 𝐼 : dom 𝐼 ⟶ 𝐸 ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ ) )
48 47 biimp3a ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ )
49 f00 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ ↔ ( ( iEdg ‘ 𝐺 ) = ∅ ∧ dom ( iEdg ‘ 𝐺 ) = ∅ ) )
50 49 simplbi ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ → ( iEdg ‘ 𝐺 ) = ∅ )
51 48 50 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( iEdg ‘ 𝐺 ) = ∅ )
52 uhgriedg0edg0 ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
53 52 3ad2ant1 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
54 51 53 mpbird ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( Edg ‘ 𝐺 ) = ∅ )