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	anim2i	$⊢ (V \in W \land a \subseteq Pairs (V)) \to (V \in W \land {I ↾}_{a} \in V)$
33	32	ancoms	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (V \in W \land {I ↾}_{a} \in V)$
34		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\})$
35	33 34	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\})$
36	29 35	mpbird	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ⟨V, {I ↾}_{a}⟩ \in USHGraph$
37		fveqeq2	$⊢ q = ⟨V, {I ↾}_{a}⟩ \to (Vtx (q) = V \leftrightarrow Vtx (⟨V, {I ↾}_{a}⟩) = V)$
38		fveqeq2	$⊢ q = ⟨V, {I ↾}_{a}⟩ \to (Edg (q) = a \leftrightarrow Edg (⟨V, {I ↾}_{a}⟩) = a)$
39	37 38	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))$
40	39	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))$
41		opvtxfv	$⊢ (V \in W \land {I ↾}_{a} \in V) \to Vtx (⟨V, {I ↾}_{a}⟩) = V$
42	32 41	syl	$⊢ (V \in W \land a \subseteq Pairs (V)) \to Vtx (⟨V, {I ↾}_{a}⟩) = V$
43		edgopval	$⊢ (V \in W \land {I ↾}_{a} \in V) \to Edg (⟨V, {I ↾}_{a}⟩) = ran ({I ↾}_{a})$
44	32 43	syl	$⊢ (V \in W \land a \subseteq Pairs (V)) \to Edg (⟨V, {I ↾}_{a}⟩) = ran ({I ↾}_{a})$
45		rnresi	$⊢ ran ({I ↾}_{a}) = a$
46	44 45	eqtrdi	$⊢ (V \in W \land a \subseteq Pairs (V)) \to Edg (⟨V, {I ↾}_{a}⟩) = a$
47	42 46	jca	$⊢ (V \in W \land a \subseteq Pairs (V)) \to (Vtx (⟨V, {I ↾}_{a}⟩) = V \land Edg (⟨V, {I ↾}_{a}⟩) = a)$
48	47	ancoms	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (Vtx (⟨V, {I ↾}_{a}⟩) = V \land Edg (⟨V, {I ↾}_{a}⟩) = a)$
49	36 40 48	rspcedvd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a)$
50	9 49	jca	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (V = V \land \exists q \in USHGraph (Vtx (q) = V \land Edg (q) = a))$
51	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))\}$
52	30	anim1i	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (a \in V \land V \in W)$
53	52	ancomd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to (V \in W \land a \in V)$
54		eqeq1	$⊢ v = V \to (v = V \leftrightarrow V = V)$
55	54	adantr	$⊢ (v = V \land e = a) \to (v = V \leftrightarrow V = V)$
56		eqeq2	$⊢ v = V \to (Vtx (q) = v \leftrightarrow Vtx (q) = V)$
57		eqeq2	$⊢ e = a \to (Edg (q) = e \leftrightarrow Edg (q) = a)$
58	56 57	bi2anan9	$⊢ (v = V \land e = a) \to ((Vtx (q) = v \land Edg (q) = e) \leftrightarrow (Vtx (q) = V \land Edg (q) = a))$
59	58	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))$
60	55 59	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)))$
61	60	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)))$
62	53 61	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)))$
63	51 62	syl5bb	$⊢ (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)))$
64	50 63	mpbird	$⊢ (a \subseteq Pairs (V) \land V \in W) \to ⟨V, a⟩ \in G$
65		fveq2	$⊢ b = ⟨V, a⟩ \to 2^{nd} (b) = 2^{nd} (⟨V, a⟩)$
66	65	eqeq2d	$⊢ b = ⟨V, a⟩ \to (a = 2^{nd} (b) \leftrightarrow a = 2^{nd} (⟨V, a⟩))$
67	66	adantl	$⊢ ((a \subseteq Pairs (V) \land V \in W) \land b = ⟨V, a⟩) \to (a = 2^{nd} (b) \leftrightarrow a = 2^{nd} (⟨V, a⟩))$
68		op2ndg	$⊢ (V \in W \land a \in V) \to 2^{nd} (⟨V, a⟩) = a$
69	68	elvd	$⊢ V \in W \to 2^{nd} (⟨V, a⟩) = a$
70	69	adantl	$⊢ (a \subseteq Pairs (V) \land V \in W) \to 2^{nd} (⟨V, a⟩) = a$
71	70	eqcomd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to a = 2^{nd} (⟨V, a⟩)$
72	64 67 71	rspcedvd	$⊢ (a \subseteq Pairs (V) \land V \in W) \to \exists b \in G a = 2^{nd} (b)$
73	72	ex	$⊢ a \subseteq Pairs (V) \to (V \in W \to \exists b \in G a = 2^{nd} (b))$
74	8 73	sylbi	$⊢ a \in P \to (V \in W \to \exists b \in G a = 2^{nd} (b))$
75	74	impcom	$⊢ (V \in W \land a \in P) \to \exists b \in G a = 2^{nd} (b)$
76	1 2 3	uspgrsprfv	$⊢ b \in G \to F (b) = 2^{nd} (b)$
77	76	adantl	$⊢ ((V \in W \land a \in P) \land b \in G) \to F (b) = 2^{nd} (b)$
78	77	eqeq2d	$⊢ ((V \in W \land a \in P) \land b \in G) \to (a = F (b) \leftrightarrow a = 2^{nd} (b))$
79	78	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))$
80	75 79	mpbird	$⊢ (V \in W \land a \in P) \to \exists b \in G a = F (b)$
81	80	ralrimiva	$⊢ V \in W \to \forall a \in P \exists b \in G a = F (b)$
82		dffo3	$⊢ F : G \underset{onto}{⟶} P \leftrightarrow (F : G ⟶ P \land \forall a \in P \exists b \in G a = F (b))$
83	5 81 82	sylanbrc	$⊢ V \in W \to F : G \underset{onto}{⟶} P$

Metamath Proof Explorer

Theorem uspgrsprfo

Proof