uhgrspan1

Description: The induced subgraph S of a hypergraph G obtained by removing one vertex is actually a subgraph of G . A subgraph is called induced orspanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in Bollobas p. 2 and section 1.1 in Diestel p. 4). (Contributed by AV, 19-Nov-2020)

	Ref	Expression
Hypotheses	uhgrspan1.v	$⊢ V = Vtx (G)$
	uhgrspan1.i	$⊢ I = iEdg (G)$
	uhgrspan1.f	$⊢ F = \{i \in dom I \| N \notin I (i)\}$
	uhgrspan1.s	$⊢ S = ⟨V ∖ \{N\}, {I ↾}_{F}⟩$
Assertion	uhgrspan1	$⊢ (G \in UHGraph \land N \in V) \to S SubGraph G$

Proof

Step	Hyp	Ref	Expression
1		uhgrspan1.v	$⊢ V = Vtx (G)$
2		uhgrspan1.i	$⊢ I = iEdg (G)$
3		uhgrspan1.f	$⊢ F = \{i \in dom I \| N \notin I (i)\}$
4		uhgrspan1.s	$⊢ S = ⟨V ∖ \{N\}, {I ↾}_{F}⟩$
5		difssd	$⊢ (G \in UHGraph \land N \in V) \to V ∖ \{N\} \subseteq V$
6	1 2 3 4	uhgrspan1lem3	$⊢ iEdg (S) = {I ↾}_{F}$
7		resresdm	$⊢ iEdg (S) = {I ↾}_{F} \to iEdg (S) = {I ↾}_{dom iEdg (S)}$
8	6 7	mp1i	$⊢ (G \in UHGraph \land N \in V) \to iEdg (S) = {I ↾}_{dom iEdg (S)}$
9	2	uhgrfun	$⊢ G \in UHGraph \to Fun I$
10		fvelima	$⊢ (Fun I \land c \in I [F]) \to \exists j \in F I (j) = c$
11	10	ex	$⊢ Fun I \to (c \in I [F] \to \exists j \in F I (j) = c)$
12	9 11	syl	$⊢ G \in UHGraph \to (c \in I [F] \to \exists j \in F I (j) = c)$
13	12	adantr	$⊢ (G \in UHGraph \land N \in V) \to (c \in I [F] \to \exists j \in F I (j) = c)$
14		eqidd	$⊢ i = j \to N = N$
15		fveq2	$⊢ i = j \to I (i) = I (j)$
16	14 15	neleq12d	$⊢ i = j \to (N \notin I (i) \leftrightarrow N \notin I (j))$
17	16 3	elrab2	$⊢ j \in F \leftrightarrow (j \in dom I \land N \notin I (j))$
18		fvexd	$⊢ ((G \in UHGraph \land N \in V) \land (j \in dom I \land N \notin I (j))) \to I (j) \in V$
19	1 2	uhgrss	$⊢ (G \in UHGraph \land j \in dom I) \to I (j) \subseteq V$
20	19	ad2ant2r	$⊢ ((G \in UHGraph \land N \in V) \land (j \in dom I \land N \notin I (j))) \to I (j) \subseteq V$
21		simprr	$⊢ ((G \in UHGraph \land N \in V) \land (j \in dom I \land N \notin I (j))) \to N \notin I (j)$
22		elpwdifsn	$⊢ (I (j) \in V \land I (j) \subseteq V \land N \notin I (j)) \to I (j) \in 𝒫 (V ∖ \{N\})$
23	18 20 21 22	syl3anc	$⊢ ((G \in UHGraph \land N \in V) \land (j \in dom I \land N \notin I (j))) \to I (j) \in 𝒫 (V ∖ \{N\})$
24		eleq1	$⊢ c = I (j) \to (c \in 𝒫 (V ∖ \{N\}) \leftrightarrow I (j) \in 𝒫 (V ∖ \{N\}))$
25	24	eqcoms	$⊢ I (j) = c \to (c \in 𝒫 (V ∖ \{N\}) \leftrightarrow I (j) \in 𝒫 (V ∖ \{N\}))$
26	23 25	syl5ibrcom	$⊢ ((G \in UHGraph \land N \in V) \land (j \in dom I \land N \notin I (j))) \to (I (j) = c \to c \in 𝒫 (V ∖ \{N\}))$
27	26	ex	$⊢ (G \in UHGraph \land N \in V) \to ((j \in dom I \land N \notin I (j)) \to (I (j) = c \to c \in 𝒫 (V ∖ \{N\})))$
28	17 27	biimtrid	$⊢ (G \in UHGraph \land N \in V) \to (j \in F \to (I (j) = c \to c \in 𝒫 (V ∖ \{N\})))$
29	28	rexlimdv	$⊢ (G \in UHGraph \land N \in V) \to (\exists j \in F I (j) = c \to c \in 𝒫 (V ∖ \{N\}))$
30	13 29	syld	$⊢ (G \in UHGraph \land N \in V) \to (c \in I [F] \to c \in 𝒫 (V ∖ \{N\}))$
31	30	ssrdv	$⊢ (G \in UHGraph \land N \in V) \to I [F] \subseteq 𝒫 (V ∖ \{N\})$
32		opex	$⊢ ⟨V ∖ \{N\}, {I ↾}_{F}⟩ \in V$
33	4 32	eqeltri	$⊢ S \in V$
34	33	a1i	$⊢ N \in V \to S \in V$
35	1 2 3 4	uhgrspan1lem2	$⊢ Vtx (S) = V ∖ \{N\}$
36	35	eqcomi	$⊢ V ∖ \{N\} = Vtx (S)$
37		eqid	$⊢ iEdg (S) = iEdg (S)$
38	6	rneqi	$⊢ ran iEdg (S) = ran ({I ↾}_{F})$
39		edgval	$⊢ Edg (S) = ran iEdg (S)$
40		df-ima	$⊢ I [F] = ran ({I ↾}_{F})$
41	38 39 40	3eqtr4ri	$⊢ I [F] = Edg (S)$
42	36 1 37 2 41	issubgr	$⊢ (G \in UHGraph \land S \in V) \to (S SubGraph G \leftrightarrow (V ∖ \{N\} \subseteq V \land iEdg (S) = {I ↾}_{dom iEdg (S)} \land I [F] \subseteq 𝒫 (V ∖ \{N\})))$
43	34 42	sylan2	$⊢ (G \in UHGraph \land N \in V) \to (S SubGraph G \leftrightarrow (V ∖ \{N\} \subseteq V \land iEdg (S) = {I ↾}_{dom iEdg (S)} \land I [F] \subseteq 𝒫 (V ∖ \{N\})))$
44	5 8 31 43	mpbir3and	$⊢ (G \in UHGraph \land N \in V) \to S SubGraph G$

Metamath Proof Explorer

Theorem uhgrspan1

Proof