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

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝐼 : 𝐴 ⟶ 𝐸 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐼 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ 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 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) )