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

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 0fi ⊢ ∅ ∈ 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 )