isubgr3stgrlem1

	Ref	Expression
Hypotheses	isubgr3stgr.v	$⊢ V = Vtx (G)$
	isubgr3stgr.u	$⊢ U = G NeighbVtx X$
	isubgr3stgr.c	$⊢ C = G ClNeighbVtx X$
	isubgr3stgr.f	$⊢ F = H \cup \{⟨X, Y⟩\}$
Assertion	isubgr3stgrlem1	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to F : C \underset{1-1 onto}{⟶} R \cup \{Y\}$

Proof

Step	Hyp	Ref	Expression
1		isubgr3stgr.v	$⊢ V = Vtx (G)$
2		isubgr3stgr.u	$⊢ U = G NeighbVtx X$
3		isubgr3stgr.c	$⊢ C = G ClNeighbVtx X$
4		isubgr3stgr.f	$⊢ F = H \cup \{⟨X, Y⟩\}$
5		f1oeq2	$⊢ U = G NeighbVtx X \to (H : U \underset{1-1 onto}{⟶} R \leftrightarrow H : G NeighbVtx X \underset{1-1 onto}{⟶} R)$
6	2 5	ax-mp	$⊢ H : U \underset{1-1 onto}{⟶} R \leftrightarrow H : G NeighbVtx X \underset{1-1 onto}{⟶} R$
7	6	biimpi	$⊢ H : U \underset{1-1 onto}{⟶} R \to H : G NeighbVtx X \underset{1-1 onto}{⟶} R$
8	7	3ad2ant1	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to H : G NeighbVtx X \underset{1-1 onto}{⟶} R$
9		simpl	$⊢ (Y \in W \land Y \notin R) \to Y \in W$
10	9	anim2i	$⊢ (X \in V \land (Y \in W \land Y \notin R)) \to (X \in V \land Y \in W)$
11	10	3adant1	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to (X \in V \land Y \in W)$
12		nbgrnself2	$⊢ X \notin (G NeighbVtx X)$
13	12	a1i	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to X \notin (G NeighbVtx X)$
14		simp3r	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to Y \notin R$
15	4	f1ounsn	$⊢ (H : G NeighbVtx X \underset{1-1 onto}{⟶} R \land (X \in V \land Y \in W) \land (X \notin (G NeighbVtx X) \land Y \notin R)) \to F : (G NeighbVtx X) \cup \{X\} \underset{1-1 onto}{⟶} R \cup \{Y\}$
16	8 11 13 14 15	syl112anc	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to F : (G NeighbVtx X) \cup \{X\} \underset{1-1 onto}{⟶} R \cup \{Y\}$
17	1	dfclnbgr4	$⊢ X \in V \to G ClNeighbVtx X = \{X\} \cup (G NeighbVtx X)$
18	17	3ad2ant2	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to G ClNeighbVtx X = \{X\} \cup (G NeighbVtx X)$
19		uncom	$⊢ \{X\} \cup (G NeighbVtx X) = (G NeighbVtx X) \cup \{X\}$
20	18 19	eqtrdi	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to G ClNeighbVtx X = (G NeighbVtx X) \cup \{X\}$
21	3 20	eqtrid	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to C = (G NeighbVtx X) \cup \{X\}$
22	21	f1oeq2d	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to (F : C \underset{1-1 onto}{⟶} R \cup \{Y\} \leftrightarrow F : (G NeighbVtx X) \cup \{X\} \underset{1-1 onto}{⟶} R \cup \{Y\})$
23	16 22	mpbird	$⊢ (H : U \underset{1-1 onto}{⟶} R \land X \in V \land (Y \in W \land Y \notin R)) \to F : C \underset{1-1 onto}{⟶} R \cup \{Y\}$

Metamath Proof Explorer

Theorem isubgr3stgrlem1

Proof