Metamath Proof Explorer


Theorem fusgrfisbase

Description: Induction base for fusgrfis . Main work is done in uhgr0v0e . (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 23-Oct-2020)

Ref Expression
Assertion fusgrfisbase ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → 𝐸 ∈ Fin )

Proof

Step Hyp Ref Expression
1 usgruhgr ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph → ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph )
2 1 3ad2ant2 ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph )
3 opvtxfv ( ( 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
4 3 3ad2ant1 ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
5 hasheq0 ( 𝑉𝑋 → ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ ) )
6 5 biimpd ( 𝑉𝑋 → ( ( ♯ ‘ 𝑉 ) = 0 → 𝑉 = ∅ ) )
7 6 adantr ( ( 𝑉𝑋𝐸𝑌 ) → ( ( ♯ ‘ 𝑉 ) = 0 → 𝑉 = ∅ ) )
8 7 a1d ( ( 𝑉𝑋𝐸𝑌 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph → ( ( ♯ ‘ 𝑉 ) = 0 → 𝑉 = ∅ ) ) )
9 8 3imp ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → 𝑉 = ∅ )
10 4 9 eqtrd ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ∅ )
11 eqid ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
12 eqid ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
13 11 12 uhgr0v0e ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph ∧ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ∅ ) → ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ∅ )
14 2 10 13 syl2anc ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ∅ )
15 0fin ∅ ∈ Fin
16 14 15 eqeltrdi ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin )
17 eqid ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
18 17 12 usgredgffibi ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) )
19 18 3ad2ant2 ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) )
20 opiedgfv ( ( 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
21 20 3ad2ant1 ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
22 21 eleq1d ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ 𝐸 ∈ Fin ) )
23 19 22 bitrd ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ 𝐸 ∈ Fin ) )
24 16 23 mpbid ( ( ( 𝑉𝑋𝐸𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → 𝐸 ∈ Fin )