Theorem lfgredgge2

Description: An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	lfuhgrnloopv.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	lfuhgrnloopv.a	⊢ 𝐴 = dom 𝐼
	lfuhgrnloopv.e	⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
Assertion	lfgredgge2	⊢ ( ( 𝐼 : 𝐴 ⟶ 𝐸 ∧ 𝑋 ∈ 𝐴 ) → 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lfuhgrnloopv.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		lfuhgrnloopv.a	⊢ 𝐴 = dom 𝐼
3		lfuhgrnloopv.e	⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
4		eqid	⊢ 𝐴 = 𝐴
5	4 3	feq23i	⊢ ( 𝐼 : 𝐴 ⟶ 𝐸 ↔ 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
6	5	biimpi	⊢ ( 𝐼 : 𝐴 ⟶ 𝐸 → 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
7	6	ffvelrnda	⊢ ( ( 𝐼 : 𝐴 ⟶ 𝐸 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐼 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
8		fveq2	⊢ ( 𝑦 = ( 𝐼 ‘ 𝑋 ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) )
9	8	breq2d	⊢ ( 𝑦 = ( 𝐼 ‘ 𝑋 ) → ( 2 ≤ ( ♯ ‘ 𝑦 ) ↔ 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) ) )
10		fveq2	⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
11	10	breq2d	⊢ ( 𝑥 = 𝑦 → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ ( ♯ ‘ 𝑦 ) ) )
12	11	cbvrabv	⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑦 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑦 ) }
13	9 12	elrab2	⊢ ( ( 𝐼 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ( ( 𝐼 ‘ 𝑋 ) ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) ) )
14	13	simprbi	⊢ ( ( 𝐼 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) )
15	7 14	syl	⊢ ( ( 𝐼 : 𝐴 ⟶ 𝐸 ∧ 𝑋 ∈ 𝐴 ) → 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) )