Theorem snstriedgval

Description: The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop for the (degenerate) case where V = ( Basendx ) . (Contributed by AV, 24-Sep-2020)

	Ref	Expression
Hypotheses	snstrvtxval.v	⊢ 𝑉 ∈ V
	snstrvtxval.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ }
Assertion	snstriedgval	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( iEdg ‘ 𝐺 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		snstrvtxval.v	⊢ 𝑉 ∈ V
2		snstrvtxval.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ }
3		iedgval	⊢ ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) )
4	3	a1i	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) )
5		necom	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) ↔ ( Base ‘ ndx ) ≠ 𝑉 )
6		fvex	⊢ ( Base ‘ ndx ) ∈ V
7	6 1 2	funsndifnop	⊢ ( ( Base ‘ ndx ) ≠ 𝑉 → ¬ 𝐺 ∈ ( V × V ) )
8	5 7	sylbi	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ 𝐺 ∈ ( V × V ) )
9	8	iffalsed	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) = ( .ef ‘ 𝐺 ) )
10		snex	⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ } ∈ V
11	10	a1i	⊢ ( 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ } → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ } ∈ V )
12	2 11	eqeltrid	⊢ ( 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ } → 𝐺 ∈ V )
13		edgfndxid	⊢ ( 𝐺 ∈ V → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )
14	2 12 13	mp2b	⊢ ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) )
15		basendxnedgfndx	⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
16	15	nesymi	⊢ ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx )
17	16	a1i	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) )
18		fvex	⊢ ( .ef ‘ ndx ) ∈ V
19	18	elsn	⊢ ( ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) } ↔ ( .ef ‘ ndx ) = ( Base ‘ ndx ) )
20	17 19	sylnibr	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) } )
21	2	dmeqi	⊢ dom 𝐺 = dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ }
22		dmsnopg	⊢ ( 𝑉 ∈ V → dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ } = { ( Base ‘ ndx ) } )
23	1 22	mp1i	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ } = { ( Base ‘ ndx ) } )
24	21 23	eqtrid	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → dom 𝐺 = { ( Base ‘ ndx ) } )
25	20 24	neleqtrrd	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 )
26		ndmfv	⊢ ( ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ )
27	25 26	syl	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ )
28	14 27	eqtrid	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( .ef ‘ 𝐺 ) = ∅ )
29	4 9 28	3eqtrd	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( iEdg ‘ 𝐺 ) = ∅ )