uspgrlimlem1

	Ref	Expression
Hypotheses	uspgrlimlem1.m	$⊢ M = H ClNeighbVtx X$
	uspgrlimlem1.j	$⊢ J = Edg (H)$
	uspgrlimlem1.l	$⊢ L = \{x \in J \| x \subseteq M\}$
Assertion	uspgrlimlem1	$⊢ H \in USHGraph \to L = iEdg (H) [\{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}]$

Proof

Step	Hyp	Ref	Expression
1		uspgrlimlem1.m	$⊢ M = H ClNeighbVtx X$
2		uspgrlimlem1.j	$⊢ J = Edg (H)$
3		uspgrlimlem1.l	$⊢ L = \{x \in J \| x \subseteq M\}$
4		eqid	$⊢ iEdg (H) = iEdg (H)$
5	4	uspgrf1oedg	$⊢ H \in USHGraph \to iEdg (H) : dom iEdg (H) \underset{1-1 onto}{⟶} Edg (H)$
6		f1of	$⊢ iEdg (H) : dom iEdg (H) \underset{1-1 onto}{⟶} Edg (H) \to iEdg (H) : dom iEdg (H) ⟶ Edg (H)$
7	5 6	syl	$⊢ H \in USHGraph \to iEdg (H) : dom iEdg (H) ⟶ Edg (H)$
8		ssrab2	$⊢ \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} \subseteq dom iEdg (H)$
9		fimarab	$⊢ (iEdg (H) : dom iEdg (H) ⟶ Edg (H) \land \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} \subseteq dom iEdg (H)) \to iEdg (H) [\{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}] = \{y \in Edg (H) \| \exists z \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} iEdg (H) (z) = y\}$
10	7 8 9	sylancl	$⊢ H \in USHGraph \to iEdg (H) [\{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}] = \{y \in Edg (H) \| \exists z \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} iEdg (H) (z) = y\}$
11	2	eqcomi	$⊢ Edg (H) = J$
12	11	a1i	$⊢ H \in USHGraph \to Edg (H) = J$
13		fveq2	$⊢ x = z \to iEdg (H) (x) = iEdg (H) (z)$
14	13	sseq1d	$⊢ x = z \to (iEdg (H) (x) \subseteq M \leftrightarrow iEdg (H) (z) \subseteq M)$
15	14	rexrab	$⊢ \exists z \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} iEdg (H) (z) = y \leftrightarrow \exists z \in dom iEdg (H) (iEdg (H) (z) \subseteq M \land iEdg (H) (z) = y)$
16		sseq1	$⊢ iEdg (H) (z) = y \to (iEdg (H) (z) \subseteq M \leftrightarrow y \subseteq M)$
17	16	biimpac	$⊢ (iEdg (H) (z) \subseteq M \land iEdg (H) (z) = y) \to y \subseteq M$
18	17	a1i	$⊢ ((H \in USHGraph \land y \in Edg (H)) \land z \in dom iEdg (H)) \to ((iEdg (H) (z) \subseteq M \land iEdg (H) (z) = y) \to y \subseteq M)$
19		f1ocnv	$⊢ iEdg (H) : dom iEdg (H) \underset{1-1 onto}{⟶} Edg (H) \to {iEdg (H)}^{-1} : Edg (H) \underset{1-1 onto}{⟶} dom iEdg (H)$
20		f1of	$⊢ {iEdg (H)}^{-1} : Edg (H) \underset{1-1 onto}{⟶} dom iEdg (H) \to {iEdg (H)}^{-1} : Edg (H) ⟶ dom iEdg (H)$
21	5 19 20	3syl	$⊢ H \in USHGraph \to {iEdg (H)}^{-1} : Edg (H) ⟶ dom iEdg (H)$
22	21	ffvelcdmda	$⊢ (H \in USHGraph \land y \in Edg (H)) \to {iEdg (H)}^{-1} (y) \in dom iEdg (H)$
23	22	adantr	$⊢ ((H \in USHGraph \land y \in Edg (H)) \land y \subseteq M) \to {iEdg (H)}^{-1} (y) \in dom iEdg (H)$
24		f1ocnvfv2	$⊢ (iEdg (H) : dom iEdg (H) \underset{1-1 onto}{⟶} Edg (H) \land y \in Edg (H)) \to iEdg (H) ({iEdg (H)}^{-1} (y)) = y$
25	5 24	sylan	$⊢ (H \in USHGraph \land y \in Edg (H)) \to iEdg (H) ({iEdg (H)}^{-1} (y)) = y$
26	25	adantr	$⊢ ((H \in USHGraph \land y \in Edg (H)) \land y \subseteq M) \to iEdg (H) ({iEdg (H)}^{-1} (y)) = y$
27		sseq1	$⊢ y = iEdg (H) ({iEdg (H)}^{-1} (y)) \to (y \subseteq M \leftrightarrow iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
28	27	eqcoms	$⊢ iEdg (H) ({iEdg (H)}^{-1} (y)) = y \to (y \subseteq M \leftrightarrow iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
29	28	biimpcd	$⊢ y \subseteq M \to (iEdg (H) ({iEdg (H)}^{-1} (y)) = y \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
30	29	adantl	$⊢ ((H \in USHGraph \land y \in Edg (H)) \land y \subseteq M) \to (iEdg (H) ({iEdg (H)}^{-1} (y)) = y \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
31	30	ancrd	$⊢ ((H \in USHGraph \land y \in Edg (H)) \land y \subseteq M) \to (iEdg (H) ({iEdg (H)}^{-1} (y)) = y \to (iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M \land iEdg (H) ({iEdg (H)}^{-1} (y)) = y))$
32	26 31	mpd	$⊢ ((H \in USHGraph \land y \in Edg (H)) \land y \subseteq M) \to (iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M \land iEdg (H) ({iEdg (H)}^{-1} (y)) = y)$
33		fveq2	$⊢ z = {iEdg (H)}^{-1} (y) \to iEdg (H) (z) = iEdg (H) ({iEdg (H)}^{-1} (y))$
34	33	sseq1d	$⊢ z = {iEdg (H)}^{-1} (y) \to (iEdg (H) (z) \subseteq M \leftrightarrow iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
35		fveqeq2	$⊢ z = {iEdg (H)}^{-1} (y) \to (iEdg (H) (z) = y \leftrightarrow iEdg (H) ({iEdg (H)}^{-1} (y)) = y)$
36	34 35	anbi12d	$⊢ z = {iEdg (H)}^{-1} (y) \to ((iEdg (H) (z) \subseteq M \land iEdg (H) (z) = y) \leftrightarrow (iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M \land iEdg (H) ({iEdg (H)}^{-1} (y)) = y))$
37	18 23 32 36	rspceb2dv	$⊢ (H \in USHGraph \land y \in Edg (H)) \to (\exists z \in dom iEdg (H) (iEdg (H) (z) \subseteq M \land iEdg (H) (z) = y) \leftrightarrow y \subseteq M)$
38	15 37	bitrid	$⊢ (H \in USHGraph \land y \in Edg (H)) \to (\exists z \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} iEdg (H) (z) = y \leftrightarrow y \subseteq M)$
39	12 38	rabeqbidva	$⊢ H \in USHGraph \to \{y \in Edg (H) \| \exists z \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\} iEdg (H) (z) = y\} = \{y \in J \| y \subseteq M\}$
40		sseq1	$⊢ y = x \to (y \subseteq M \leftrightarrow x \subseteq M)$
41	40	cbvrabv	$⊢ \{y \in J \| y \subseteq M\} = \{x \in J \| x \subseteq M\}$
42	41	a1i	$⊢ H \in USHGraph \to \{y \in J \| y \subseteq M\} = \{x \in J \| x \subseteq M\}$
43	10 39 42	3eqtrrd	$⊢ H \in USHGraph \to \{x \in J \| x \subseteq M\} = iEdg (H) [\{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}]$
44	3 43	eqtrid	$⊢ H \in USHGraph \to L = iEdg (H) [\{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}]$

Metamath Proof Explorer

Theorem uspgrlimlem1

Proof