Theorem structiedg0val

Description: The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	structvtxvallem.s	⊢ 𝑆 ∈ ℕ
	structvtxvallem.b	⊢ ( Base ‘ ndx ) < 𝑆
	structvtxvallem.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
Assertion	structiedg0val	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	⊢ 𝑆 ∈ ℕ
2		structvtxvallem.b	⊢ ( Base ‘ ndx ) < 𝑆
3		structvtxvallem.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
4	3 2 1	2strstr1	⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩
5		structn0fun	⊢ ( 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩ → Fun ( 𝐺 ∖ { ∅ } ) )
6	1 2 3	structvtxvallem	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
7		funiedgdmge2val	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
8	5 6 7	syl2an	⊢ ( ( 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩ ∧ ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
9	4 8	mpan	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
10	9	3adant3	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
11		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ∈ V
12	11	a1i	⊢ ( 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ∈ V )
13	3 12	eqeltrid	⊢ ( 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } → 𝐺 ∈ V )
14		edgfndxid	⊢ ( 𝐺 ∈ V → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )
15	3 13 14	mp2b	⊢ ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) )
16		basendxnedgfndx	⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
17	16	nesymi	⊢ ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx )
18	17	a1i	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) )
19		neneq	⊢ ( 𝑆 ≠ ( .ef ‘ ndx ) → ¬ 𝑆 = ( .ef ‘ ndx ) )
20		eqcom	⊢ ( ( .ef ‘ ndx ) = 𝑆 ↔ 𝑆 = ( .ef ‘ ndx ) )
21	19 20	sylnibr	⊢ ( 𝑆 ≠ ( .ef ‘ ndx ) → ¬ ( .ef ‘ ndx ) = 𝑆 )
22	21	3ad2ant3	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) = 𝑆 )
23		ioran	⊢ ( ¬ ( ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∨ ( .ef ‘ ndx ) = 𝑆 ) ↔ ( ¬ ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∧ ¬ ( .ef ‘ ndx ) = 𝑆 ) )
24	18 22 23	sylanbrc	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∨ ( .ef ‘ ndx ) = 𝑆 ) )
25		fvex	⊢ ( .ef ‘ ndx ) ∈ V
26	25	elpr	⊢ ( ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) , 𝑆 } ↔ ( ( .ef ‘ ndx ) = ( Base ‘ ndx ) ∨ ( .ef ‘ ndx ) = 𝑆 ) )
27	24 26	sylnibr	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) ∈ { ( Base ‘ ndx ) , 𝑆 } )
28	3	dmeqi	⊢ dom 𝐺 = dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
29		dmpropg	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } = { ( Base ‘ ndx ) , 𝑆 } )
30	29	3adant3	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → dom { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } = { ( Base ‘ ndx ) , 𝑆 } )
31	28 30	eqtrid	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → dom 𝐺 = { ( Base ‘ ndx ) , 𝑆 } )
32	27 31	neleqtrrd	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 )
33		ndmfv	⊢ ( ¬ ( .ef ‘ ndx ) ∈ dom 𝐺 → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ )
34	32 33	syl	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ∅ )
35	15 34	eqtrid	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( .ef ‘ 𝐺 ) = ∅ )
36	10 35	eqtrd	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ ( .ef ‘ ndx ) ) → ( iEdg ‘ 𝐺 ) = ∅ )