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	$⊢ S \in ℕ$
	structvtxvallem.b	$⊢ {Base}_{ndx} < S$
	structvtxvallem.g	$⊢ G = \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\}$
Assertion	structiedg0val	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to iEdg (G) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	$⊢ S \in ℕ$
2		structvtxvallem.b	$⊢ {Base}_{ndx} < S$
3		structvtxvallem.g	$⊢ G = \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\}$
4	3 2 1	2strstr1	$⊢ G Struct ⟨{Base}_{ndx}, S⟩$
5		structn0fun	$⊢ G Struct ⟨{Base}_{ndx}, S⟩ \to Fun (G ∖ \{\emptyset\})$
6	1 2 3	structvtxvallem	$⊢ (V \in X \land E \in Y) \to 2 \leq \|dom G\|$
7		funiedgdmge2val	$⊢ (Fun (G ∖ \{\emptyset\}) \land 2 \leq \|dom G\|) \to iEdg (G) = ef (G)$
8	5 6 7	syl2an	$⊢ (G Struct ⟨{Base}_{ndx}, S⟩ \land (V \in X \land E \in Y)) \to iEdg (G) = ef (G)$
9	4 8	mpan	$⊢ (V \in X \land E \in Y) \to iEdg (G) = ef (G)$
10	9	3adant3	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to iEdg (G) = ef (G)$
11		prex	$⊢ \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\} \in V$
12	11	a1i	$⊢ G = \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\} \to \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\} \in V$
13	3 12	eqeltrid	$⊢ G = \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\} \to G \in V$
14		edgfndxid	$⊢ G \in V \to ef (G) = G (ef (ndx))$
15	3 13 14	mp2b	$⊢ ef (G) = G (ef (ndx))$
16		basendxnedgfndx	$⊢ {Base}_{ndx} \neq ef (ndx)$
17	16	nesymi	$⊢ \neg ef (ndx) = {Base}_{ndx}$
18	17	a1i	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to \neg ef (ndx) = {Base}_{ndx}$
19		neneq	$⊢ S \neq ef (ndx) \to \neg S = ef (ndx)$
20		eqcom	$⊢ ef (ndx) = S \leftrightarrow S = ef (ndx)$
21	19 20	sylnibr	$⊢ S \neq ef (ndx) \to \neg ef (ndx) = S$
22	21	3ad2ant3	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to \neg ef (ndx) = S$
23		ioran	$⊢ \neg (ef (ndx) = {Base}_{ndx} \lor ef (ndx) = S) \leftrightarrow (\neg ef (ndx) = {Base}_{ndx} \land \neg ef (ndx) = S)$
24	18 22 23	sylanbrc	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to \neg (ef (ndx) = {Base}_{ndx} \lor ef (ndx) = S)$
25		fvex	$⊢ ef (ndx) \in V$
26	25	elpr	$⊢ ef (ndx) \in \{{Base}_{ndx}, S\} \leftrightarrow (ef (ndx) = {Base}_{ndx} \lor ef (ndx) = S)$
27	24 26	sylnibr	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to \neg ef (ndx) \in \{{Base}_{ndx}, S\}$
28	3	dmeqi	$⊢ dom G = dom \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\}$
29		dmpropg	$⊢ (V \in X \land E \in Y) \to dom \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\} = \{{Base}_{ndx}, S\}$
30	29	3adant3	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to dom \{⟨{Base}_{ndx}, V⟩, ⟨S, E⟩\} = \{{Base}_{ndx}, S\}$
31	28 30	eqtrid	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to dom G = \{{Base}_{ndx}, S\}$
32	27 31	neleqtrrd	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to \neg ef (ndx) \in dom G$
33		ndmfv	$⊢ \neg ef (ndx) \in dom G \to G (ef (ndx)) = \emptyset$
34	32 33	syl	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to G (ef (ndx)) = \emptyset$
35	15 34	eqtrid	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to ef (G) = \emptyset$
36	10 35	eqtrd	$⊢ (V \in X \land E \in Y \land S \neq ef (ndx)) \to iEdg (G) = \emptyset$

Metamath Proof Explorer

Theorem structiedg0val

Proof