uspgrsprf

Description: The mapping F is a function from the "simple pseudographs" with a fixed set of vertices V into the subsets of the set of pairs over the set V . (Contributed by AV, 24-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	uspgrsprf	$⊢ F : G ⟶ 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	2	eleq2i	$⊢ g \in G \leftrightarrow g \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\}$
5		elopab	$⊢ g \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\} \leftrightarrow \exists v \exists e (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)))$
6	4 5	bitri	$⊢ g \in G \leftrightarrow \exists v \exists e (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)))$
7		uspgrupgr	$⊢ q \in USHGraph \to q \in UPGraph$
8		upgredgssspr	$⊢ q \in UPGraph \to Edg (q) \subseteq Pairs (Vtx (q))$
9	7 8	syl	$⊢ q \in USHGraph \to Edg (q) \subseteq Pairs (Vtx (q))$
10	9	adantr	$⊢ (q \in USHGraph \land (Vtx (q) = v \land Edg (q) = e)) \to Edg (q) \subseteq Pairs (Vtx (q))$
11		simpr	$⊢ (Vtx (q) = v \land Edg (q) = e) \to Edg (q) = e$
12		fveq2	$⊢ Vtx (q) = v \to Pairs (Vtx (q)) = Pairs (v)$
13	12	adantr	$⊢ (Vtx (q) = v \land Edg (q) = e) \to Pairs (Vtx (q)) = Pairs (v)$
14	11 13	sseq12d	$⊢ (Vtx (q) = v \land Edg (q) = e) \to (Edg (q) \subseteq Pairs (Vtx (q)) \leftrightarrow e \subseteq Pairs (v))$
15	14	adantl	$⊢ (q \in USHGraph \land (Vtx (q) = v \land Edg (q) = e)) \to (Edg (q) \subseteq Pairs (Vtx (q)) \leftrightarrow e \subseteq Pairs (v))$
16	10 15	mpbid	$⊢ (q \in USHGraph \land (Vtx (q) = v \land Edg (q) = e)) \to e \subseteq Pairs (v)$
17	16	rexlimiva	$⊢ \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e) \to e \subseteq Pairs (v)$
18	17	adantl	$⊢ (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)) \to e \subseteq Pairs (v)$
19		fveq2	$⊢ v = V \to Pairs (v) = Pairs (V)$
20	19	sseq2d	$⊢ v = V \to (e \subseteq Pairs (v) \leftrightarrow e \subseteq Pairs (V))$
21	20	adantr	$⊢ (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)) \to (e \subseteq Pairs (v) \leftrightarrow e \subseteq Pairs (V))$
22	18 21	mpbid	$⊢ (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)) \to e \subseteq Pairs (V)$
23	22	adantl	$⊢ (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to e \subseteq Pairs (V)$
24		vex	$⊢ v \in V$
25		vex	$⊢ e \in V$
26	24 25	op2ndd	$⊢ g = ⟨v, e⟩ \to 2^{nd} (g) = e$
27	26	sseq1d	$⊢ g = ⟨v, e⟩ \to (2^{nd} (g) \subseteq Pairs (V) \leftrightarrow e \subseteq Pairs (V))$
28	27	adantr	$⊢ (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to (2^{nd} (g) \subseteq Pairs (V) \leftrightarrow e \subseteq Pairs (V))$
29	23 28	mpbird	$⊢ (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to 2^{nd} (g) \subseteq Pairs (V)$
30	1	eleq2i	$⊢ 2^{nd} (g) \in P \leftrightarrow 2^{nd} (g) \in 𝒫 Pairs (V)$
31		fvex	$⊢ 2^{nd} (g) \in V$
32	31	elpw	$⊢ 2^{nd} (g) \in 𝒫 Pairs (V) \leftrightarrow 2^{nd} (g) \subseteq Pairs (V)$
33	30 32	bitri	$⊢ 2^{nd} (g) \in P \leftrightarrow 2^{nd} (g) \subseteq Pairs (V)$
34	29 33	sylibr	$⊢ (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to 2^{nd} (g) \in P$
35	34	exlimivv	$⊢ \exists v \exists e (g = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to 2^{nd} (g) \in P$
36	6 35	sylbi	$⊢ g \in G \to 2^{nd} (g) \in P$
37	3 36	fmpti	$⊢ F : G ⟶ P$

Metamath Proof Explorer

Theorem uspgrsprf

Proof