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 )