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 ⊢ I = iEdg ⁡ G
lfuhgrnloopv.a ⊢ A = dom ⁡ I
lfuhgrnloopv.e ⊢ E = x ∈ 𝒫 V | 2 ≤ x
Assertion lfgredgge2 ⊢ I : A ⟶ E ∧ X ∈ A → 2 ≤ I ⁡ X

Proof

Step Hyp Ref Expression
1 lfuhgrnloopv.i ⊢ I = iEdg ⁡ G
2 lfuhgrnloopv.a ⊢ A = dom ⁡ I
3 lfuhgrnloopv.e ⊢ E = x ∈ 𝒫 V | 2 ≤ x
4 eqid ⊢ A = A
5 4 3 feq23i ⊢ I : A ⟶ E ↔ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x
6 5 biimpi ⊢ I : A ⟶ E → I : A ⟶ x ∈ 𝒫 V | 2 ≤ x
7 6 ffvelcdmda ⊢ I : A ⟶ E ∧ X ∈ A → I ⁡ X ∈ x ∈ 𝒫 V | 2 ≤ x
8 fveq2 ⊢ y = I ⁡ X → y = I ⁡ X
9 8 breq2d ⊢ y = I ⁡ X → 2 ≤ y ↔ 2 ≤ I ⁡ X
10 fveq2 ⊢ x = y → x = y
11 10 breq2d ⊢ x = y → 2 ≤ x ↔ 2 ≤ y
12 11 cbvrabv ⊢ x ∈ 𝒫 V | 2 ≤ x = y ∈ 𝒫 V | 2 ≤ y
13 9 12 elrab2 ⊢ I ⁡ X ∈ x ∈ 𝒫 V | 2 ≤ x ↔ I ⁡ X ∈ 𝒫 V ∧ 2 ≤ I ⁡ X
14 13 simprbi ⊢ I ⁡ X ∈ x ∈ 𝒫 V | 2 ≤ x → 2 ≤ I ⁡ X
15 7 14 syl ⊢ I : A ⟶ E ∧ X ∈ A → 2 ≤ I ⁡ X