uspgrsprfo

Description: The mapping F is a function from the "simple pseudographs" with a fixed set of vertices V onto the subsets of the set of pairs over the set V . (Contributed by AV, 25-Nov-2021)

	Ref	Expression
Hypotheses	uspgrsprf.p	$⊢ P = 𝒫 Pairs (V)$
	uspgrsprf.g	$⊢ G = \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\}$
	uspgrsprf.f	$⊢ F = (g \in G ⟼ 2^{nd} (g))$
Assertion	uspgrsprfo	$⊢ V \in W \to F : G \underset{onto}{⟶} P$

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	$⊢ P = 𝒫 Pairs (V)$
2		uspgrsprf.g	$⊢ G = \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\}$
3		uspgrsprf.f	$⊢ F = (g \in G ⟼ 2^{nd} (g))$
4	1 2 3	uspgrsprf	$⊢ F : G ⟶ P$
5	4	a1i	$⊢ V \in W \to F : G ⟶ P$
6	1	eleq2i	$⊢ a \in P \leftrightarrow a \in 𝒫 Pairs (V)$
7		velpw	$⊢ a \in 𝒫 Pairs (V) \leftrightarrow a \subseteq Pairs (V)$
8	6 7	bitri	$⊢ a \in P \leftrightarrow a \subseteq Pairs (V)$
9		eqidd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to V = V$
10		vex	$⊢ a \in V$
11	10	a1i	$⊢ (a \subseteq Pairs (V) \land V \in W) \to a \in V$
12		f1oi	$⊢ ({I ↾}_{a}) : a \underset{1-1 onto}{⟶} a$
13	12	a1i	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ({I ↾}_{a}) : a \underset{1-1 onto}{⟶} a$
14		dmresi	$⊢ dom ({I ↾}_{a}) = a$
15		f1oeq2	$⊢ dom ({I ↾}_{a}) = a \to (({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} a \leftrightarrow ({I ↾}_{a}) : a \underset{1-1 onto}{⟶} a)$
16	14 15	ax-mp	$⊢ ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} a \leftrightarrow ({I ↾}_{a}) : a \underset{1-1 onto}{⟶} a$
17	13 16	sylibr	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} a$
18		sprvalpwle2	$⊢ V \in W \to Pairs (V) = \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\}$
19	18	sseq2d	$⊢ V \in W \to (a \subseteq Pairs (V) \leftrightarrow a \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
20	19	biimpac	$⊢ (a \subseteq Pairs (V) \land V \in W) \to a \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\}$
21	17 20	jca	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} a \land a \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
22		f1oeq3	$⊢ f = a \to (({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} f \leftrightarrow ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} a)$
23		sseq1	$⊢ f = a \to (f \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\} \leftrightarrow a \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
24	22 23	anbi12d	$⊢ f = a \to ((({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} f \land f \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\}) \leftrightarrow (({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} a \land a \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\}))$
25	11 21 24	spcedv	$⊢ (a \subseteq Pairs (V) \land V \in W) \to \exists f (({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} f \land f \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
26		resiexg	$⊢ a \in V \to {I ↾}_{a} \in V$
27	10 26	ax-mp	$⊢ {I ↾}_{a} \in V$
28	27	f11o	$⊢ ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1}{⟶} \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\} \leftrightarrow \exists f (({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1 onto}{⟶} f \land f \subseteq \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
29	25 28	sylibr	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1}{⟶} \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\}$
30	10	a1i	$⊢ a \subseteq Pairs (V) \to a \in V$
31	30	resiexd	$⊢ a \subseteq Pairs (V) \to {I ↾}_{a} \in V$
32	31	anim1ci	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (V \in W \land {I ↾}_{a} \in V)$
33		isuspgrop	$⊢ (V \in W \land {I ↾}_{a} \in V) \to (⟨V, {I ↾}_{a}⟩ \in USHGraph \leftrightarrow ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1}{⟶} \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
34	32 33	syl	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (⟨V, {I ↾}_{a}⟩ \in USHGraph \leftrightarrow ({I ↾}_{a}) : dom ({I ↾}_{a}) \underset{1-1}{⟶} \{p \in (𝒫 V ∖ \{\emptyset\}) \| \|p\| \leq 2\})$
35	29 34	mpbird	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ⟨V, {I ↾}_{a}⟩ \in USHGraph$
36		fveqeq2	$⊢ q = ⟨V, {I ↾}_{a}⟩ \to (Vtx (q) = V \leftrightarrow Vtx (⟨V, {I ↾}_{a}⟩) = V)$
37		fveqeq2	$⊢ q = ⟨V, {I ↾}_{a}⟩ \to (Edg (q) = a \leftrightarrow Edg (⟨V, {I ↾}_{a}⟩) = a)$
38	36 37	anbi12d	$⊢ q = ⟨V, {I ↾}_{a}⟩ \to ((Vtx (q) = V \land Edg (q) = a) \leftrightarrow (Vtx (⟨V, {I ↾}_{a}⟩) = V \land Edg (⟨V, {I ↾}_{a}⟩) = a))$
39	38	adantl	$⊢ ((a \subseteq Pairs (V) \land V \in W) \land q = ⟨V, {I ↾}_{a}⟩) \to ((Vtx (q) = V \land Edg (q) = a) \leftrightarrow (Vtx (⟨V, {I ↾}_{a}⟩) = V \land Edg (⟨V, {I ↾}_{a}⟩) = a))$
40		opvtxfv	$⊢ (V \in W \land {I ↾}_{a} \in V) \to Vtx (⟨V, {I ↾}_{a}⟩) = V$
41	31 40	sylan2	$⊢ (V \in W \land a \subseteq Pairs (V)) \to Vtx (⟨V, {I ↾}_{a}⟩) = V$
42		edgopval	$⊢ (V \in W \land {I ↾}_{a} \in V) \to Edg (⟨V, {I ↾}_{a}⟩) = ran ({I ↾}_{a})$
43	31 42	sylan2	$⊢ (V \in W \land a \subseteq Pairs (V)) \to Edg (⟨V, {I ↾}_{a}⟩) = ran ({I ↾}_{a})$
44		rnresi	$⊢ ran ({I ↾}_{a}) = a$
45	43 44	eqtrdi	$⊢ (V \in W \land a \subseteq Pairs (V)) \to Edg (⟨V, {I ↾}_{a}⟩) = a$
46	41 45	jca	$⊢ (V \in W \land a \subseteq Pairs (V)) \to (Vtx (⟨V, {I ↾}_{a}⟩) = V \land Edg (⟨V, {I ↾}_{a}⟩) = a)$
47	46	ancoms	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (Vtx (⟨V, {I ↾}_{a}⟩) = V \land Edg (⟨V, {I ↾}_{a}⟩) = a)$
48	35 39 47	rspcedvd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a)$
49	9 48	jca	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (V = V \land \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a))$
50	2	eleq2i	$⊢ ⟨V, a⟩ \in G \leftrightarrow ⟨V, a⟩ \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\}$
51	30	anim1ci	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (V \in W \land a \in V)$
52		eqeq1	$⊢ v = V \to (v = V \leftrightarrow V = V)$
53	52	adantr	$⊢ (v = V \land e = a) \to (v = V \leftrightarrow V = V)$
54		eqeq2	$⊢ v = V \to (Vtx (q) = v \leftrightarrow Vtx (q) = V)$
55		eqeq2	$⊢ e = a \to (Edg (q) = e \leftrightarrow Edg (q) = a)$
56	54 55	bi2anan9	$⊢ (v = V \land e = a) \to ((Vtx (q) = v \land Edg (q) = e) \leftrightarrow (Vtx (q) = V \land Edg (q) = a))$
57	56	rexbidv	$⊢ (v = V \land e = a) \to (\exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e) \leftrightarrow \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a))$
58	53 57	anbi12d	$⊢ (v = V \land e = a) \to ((v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)) \leftrightarrow (V = V \land \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a)))$
59	58	opelopabga	$⊢ (V \in W \land a \in V) \to (⟨V, a⟩ \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\} \leftrightarrow (V = V \land \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a)))$
60	51 59	syl	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (⟨V, a⟩ \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\} \leftrightarrow (V = V \land \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a)))$
61	50 60	bitrid	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (⟨V, a⟩ \in G \leftrightarrow (V = V \land \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a)))$
62	49 61	mpbird	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ⟨V, a⟩ \in G$
63		fveq2	$⊢ b = ⟨V, a⟩ \to 2^{nd} (b) = 2^{nd} (⟨V, a⟩)$
64	63	eqeq2d	$⊢ b = ⟨V, a⟩ \to (a = 2^{nd} (b) \leftrightarrow a = 2^{nd} (⟨V, a⟩))$
65	64	adantl	$⊢ ((a \subseteq Pairs (V) \land V \in W) \land b = ⟨V, a⟩) \to (a = 2^{nd} (b) \leftrightarrow a = 2^{nd} (⟨V, a⟩))$
66		op2ndg	$⊢ (V \in W \land a \in V) \to 2^{nd} (⟨V, a⟩) = a$
67	66	elvd	$⊢ V \in W \to 2^{nd} (⟨V, a⟩) = a$
68	67	adantl	$⊢ (a \subseteq Pairs (V) \land V \in W) \to 2^{nd} (⟨V, a⟩) = a$
69	68	eqcomd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to a = 2^{nd} (⟨V, a⟩)$
70	62 65 69	rspcedvd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to \exists b \in G a = 2^{nd} (b)$
71	70	ex	$⊢ a \subseteq Pairs (V) \to (V \in W \to \exists b \in G a = 2^{nd} (b))$
72	8 71	sylbi	$⊢ a \in P \to (V \in W \to \exists b \in G a = 2^{nd} (b))$
73	72	impcom	$⊢ (V \in W \land a \in P) \to \exists b \in G a = 2^{nd} (b)$
74	1 2 3	uspgrsprfv	$⊢ b \in G \to F (b) = 2^{nd} (b)$
75	74	adantl	$⊢ ((V \in W \land a \in P) \land b \in G) \to F (b) = 2^{nd} (b)$
76	75	eqeq2d	$⊢ ((V \in W \land a \in P) \land b \in G) \to (a = F (b) \leftrightarrow a = 2^{nd} (b))$
77	76	rexbidva	$⊢ (V \in W \land a \in P) \to (\exists b \in G a = F (b) \leftrightarrow \exists b \in G a = 2^{nd} (b))$
78	73 77	mpbird	$⊢ (V \in W \land a \in P) \to \exists b \in G a = F (b)$
79	78	ralrimiva	$⊢ V \in W \to \forall a \in P \exists b \in G a = F (b)$
80		dffo3	$⊢ F : G \underset{onto}{⟶} P \leftrightarrow (F : G ⟶ P \land \forall a \in P \exists b \in G a = F (b))$
81	5 79 80	sylanbrc	$⊢ V \in W \to F : G \underset{onto}{⟶} P$

Metamath Proof Explorer

Theorem uspgrsprfo

Proof