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		snex	⊢ { 𝑣 } ∈ 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	syl5eq	⊢ ( ( 𝐺 ∈ 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 ‘ 𝐺 ) = ∅ )