uspgrlimlem2

	Ref	Expression
Hypotheses	uspgrlimlem1.m	$⊢ M = H ClNeighbVtx X$
	uspgrlimlem1.j	$⊢ J = Edg (H)$
	uspgrlimlem1.l	$⊢ L = \{x \in J \| x \subseteq M\}$
Assertion	uspgrlimlem2	$⊢ H \in USHGraph \to {iEdg (H)}^{-1} [L] = \{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		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)$
7		f1of	$⊢ {iEdg (H)}^{-1} : Edg (H) \underset{1-1 onto}{⟶} dom iEdg (H) \to {iEdg (H)}^{-1} : Edg (H) ⟶ dom iEdg (H)$
8	5 6 7	3syl	$⊢ H \in USHGraph \to {iEdg (H)}^{-1} : Edg (H) ⟶ dom iEdg (H)$
9	2	rabeqi	$⊢ \{x \in J \| x \subseteq M\} = \{x \in Edg (H) \| x \subseteq M\}$
10	3 9	eqtri	$⊢ L = \{x \in Edg (H) \| x \subseteq M\}$
11	10	ssrab3	$⊢ L \subseteq Edg (H)$
12		fimarab	$⊢ ({iEdg (H)}^{-1} : Edg (H) ⟶ dom iEdg (H) \land L \subseteq Edg (H)) \to {iEdg (H)}^{-1} [L] = \{x \in dom iEdg (H) \| \exists y \in L {iEdg (H)}^{-1} (y) = x\}$
13	8 11 12	sylancl	$⊢ H \in USHGraph \to {iEdg (H)}^{-1} [L] = \{x \in dom iEdg (H) \| \exists y \in L {iEdg (H)}^{-1} (y) = x\}$
14		sseq1	$⊢ x = y \to (x \subseteq M \leftrightarrow y \subseteq M)$
15	14 3	elrab2	$⊢ y \in L \leftrightarrow (y \in J \land y \subseteq M)$
16	2	eleq2i	$⊢ y \in J \leftrightarrow y \in Edg (H)$
17	16	biimpi	$⊢ y \in J \to y \in Edg (H)$
18		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$
19	5 17 18	syl2an	$⊢ (H \in USHGraph \land y \in J) \to iEdg (H) ({iEdg (H)}^{-1} (y)) = y$
20	19	eqcomd	$⊢ (H \in USHGraph \land y \in J) \to y = iEdg (H) ({iEdg (H)}^{-1} (y))$
21	20	sseq1d	$⊢ (H \in USHGraph \land y \in J) \to (y \subseteq M \leftrightarrow iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
22	21	biimpd	$⊢ (H \in USHGraph \land y \in J) \to (y \subseteq M \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M)$
23	22	ex	$⊢ H \in USHGraph \to (y \in J \to (y \subseteq M \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M))$
24	23	adantr	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to (y \in J \to (y \subseteq M \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M))$
25	24	imp32	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land (y \in J \land y \subseteq M)) \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M$
26	25	3adant3	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land (y \in J \land y \subseteq M) \land {iEdg (H)}^{-1} (y) = x) \to iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M$
27		fveq2	$⊢ {iEdg (H)}^{-1} (y) = x \to iEdg (H) ({iEdg (H)}^{-1} (y)) = iEdg (H) (x)$
28	27	sseq1d	$⊢ {iEdg (H)}^{-1} (y) = x \to (iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M \leftrightarrow iEdg (H) (x) \subseteq M)$
29	28	3ad2ant3	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land (y \in J \land y \subseteq M) \land {iEdg (H)}^{-1} (y) = x) \to (iEdg (H) ({iEdg (H)}^{-1} (y)) \subseteq M \leftrightarrow iEdg (H) (x) \subseteq M)$
30	26 29	mpbid	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land (y \in J \land y \subseteq M) \land {iEdg (H)}^{-1} (y) = x) \to iEdg (H) (x) \subseteq M$
31	30	3exp	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to ((y \in J \land y \subseteq M) \to ({iEdg (H)}^{-1} (y) = x \to iEdg (H) (x) \subseteq M))$
32	15 31	biimtrid	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to (y \in L \to ({iEdg (H)}^{-1} (y) = x \to iEdg (H) (x) \subseteq M))$
33	32	rexlimdv	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to (\exists y \in L {iEdg (H)}^{-1} (y) = x \to iEdg (H) (x) \subseteq M)$
34		fveqeq2	$⊢ y = iEdg (H) (x) \to ({iEdg (H)}^{-1} (y) = x \leftrightarrow {iEdg (H)}^{-1} (iEdg (H) (x)) = x)$
35		f1of	$⊢ iEdg (H) : dom iEdg (H) \underset{1-1 onto}{⟶} Edg (H) \to iEdg (H) : dom iEdg (H) ⟶ Edg (H)$
36		eqid	$⊢ dom iEdg (H) = dom iEdg (H)$
37	2	eqcomi	$⊢ Edg (H) = J$
38	36 37	feq23i	$⊢ iEdg (H) : dom iEdg (H) ⟶ Edg (H) \leftrightarrow iEdg (H) : dom iEdg (H) ⟶ J$
39	38	biimpi	$⊢ iEdg (H) : dom iEdg (H) ⟶ Edg (H) \to iEdg (H) : dom iEdg (H) ⟶ J$
40	5 35 39	3syl	$⊢ H \in USHGraph \to iEdg (H) : dom iEdg (H) ⟶ J$
41	40	ffvelcdmda	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to iEdg (H) (x) \in J$
42	41	anim1i	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land iEdg (H) (x) \subseteq M) \to (iEdg (H) (x) \in J \land iEdg (H) (x) \subseteq M)$
43		sseq1	$⊢ y = iEdg (H) (x) \to (y \subseteq M \leftrightarrow iEdg (H) (x) \subseteq M)$
44	14 43 3	elrab2w	$⊢ iEdg (H) (x) \in L \leftrightarrow (iEdg (H) (x) \in J \land iEdg (H) (x) \subseteq M)$
45	42 44	sylibr	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land iEdg (H) (x) \subseteq M) \to iEdg (H) (x) \in L$
46		f1ocnvfv1	$⊢ (iEdg (H) : dom iEdg (H) \underset{1-1 onto}{⟶} Edg (H) \land x \in dom iEdg (H)) \to {iEdg (H)}^{-1} (iEdg (H) (x)) = x$
47	5 46	sylan	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to {iEdg (H)}^{-1} (iEdg (H) (x)) = x$
48	47	adantr	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land iEdg (H) (x) \subseteq M) \to {iEdg (H)}^{-1} (iEdg (H) (x)) = x$
49	34 45 48	rspcedvdw	$⊢ ((H \in USHGraph \land x \in dom iEdg (H)) \land iEdg (H) (x) \subseteq M) \to \exists y \in L {iEdg (H)}^{-1} (y) = x$
50	49	ex	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to (iEdg (H) (x) \subseteq M \to \exists y \in L {iEdg (H)}^{-1} (y) = x)$
51	33 50	impbid	$⊢ (H \in USHGraph \land x \in dom iEdg (H)) \to (\exists y \in L {iEdg (H)}^{-1} (y) = x \leftrightarrow iEdg (H) (x) \subseteq M)$
52	51	rabbidva	$⊢ H \in USHGraph \to \{x \in dom iEdg (H) \| \exists y \in L {iEdg (H)}^{-1} (y) = x\} = \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}$
53	13 52	eqtrd	$⊢ H \in USHGraph \to {iEdg (H)}^{-1} [L] = \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq M\}$

Metamath Proof Explorer

Theorem uspgrlimlem2

Proof