uspgrsprf1

Description: The mapping F is a one-to-one 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, 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	uspgrsprf1	$⊢ F : G \underset{1-1}{⟶} 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	1 2 3	uspgrsprfv	$⊢ a \in G \to F (a) = 2^{nd} (a)$
6	1 2 3	uspgrsprfv	$⊢ b \in G \to F (b) = 2^{nd} (b)$
7	5 6	eqeqan12d	$⊢ (a \in G \land b \in G) \to (F (a) = F (b) \leftrightarrow 2^{nd} (a) = 2^{nd} (b))$
8	2	eleq2i	$⊢ a \in G \leftrightarrow a \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\}$
9		elopab	$⊢ a \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\} \leftrightarrow \exists v \exists e (a = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)))$
10		opeq12	$⊢ (v = w \land e = f) \to ⟨v, e⟩ = ⟨w, f⟩$
11	10	eqeq2d	$⊢ (v = w \land e = f) \to (a = ⟨v, e⟩ \leftrightarrow a = ⟨w, f⟩)$
12		eqeq1	$⊢ v = w \to (v = V \leftrightarrow w = V)$
13	12	adantr	$⊢ (v = w \land e = f) \to (v = V \leftrightarrow w = V)$
14		eqeq2	$⊢ v = w \to (Vtx (q) = v \leftrightarrow Vtx (q) = w)$
15		eqeq2	$⊢ e = f \to (Edg (q) = e \leftrightarrow Edg (q) = f)$
16	14 15	bi2anan9	$⊢ (v = w \land e = f) \to ((Vtx (q) = v \land Edg (q) = e) \leftrightarrow (Vtx (q) = w \land Edg (q) = f))$
17	16	rexbidv	$⊢ (v = w \land e = f) \to (\exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e) \leftrightarrow \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))$
18	13 17	anbi12d	$⊢ (v = w \land e = f) \to ((v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)) \leftrightarrow (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))$
19	11 18	anbi12d	$⊢ (v = w \land e = f) \to ((a = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \leftrightarrow (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))))$
20	19	cbvex2vw	$⊢ \exists v \exists e (a = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \leftrightarrow \exists w \exists f (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))$
21	8 9 20	3bitri	$⊢ a \in G \leftrightarrow \exists w \exists f (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))$
22	2	eleq2i	$⊢ b \in G \leftrightarrow b \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\}$
23		elopab	$⊢ b \in \{⟨v, e⟩ \| (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))\} \leftrightarrow \exists v \exists e (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)))$
24	22 23	bitri	$⊢ b \in G \leftrightarrow \exists v \exists e (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)))$
25		eqeq2	$⊢ w = V \to (v = w \leftrightarrow v = V)$
26		opeq12	$⊢ (w = v \land f = e) \to ⟨w, f⟩ = ⟨v, e⟩$
27	26	ex	$⊢ w = v \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩)$
28	27	equcoms	$⊢ v = w \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩)$
29	25 28	syl6bir	$⊢ w = V \to (v = V \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩))$
30	29	ad2antrl	$⊢ (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (v = V \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩))$
31	30	com12	$⊢ v = V \to ((a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩))$
32	31	ad2antrl	$⊢ (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to ((a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩))$
33	32	imp	$⊢ ((b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \land (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))) \to (f = e \to ⟨w, f⟩ = ⟨v, e⟩)$
34		vex	$⊢ w \in V$
35		vex	$⊢ f \in V$
36	34 35	op2ndd	$⊢ a = ⟨w, f⟩ \to 2^{nd} (a) = f$
37	36	ad2antrl	$⊢ ((b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \land (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))) \to 2^{nd} (a) = f$
38		vex	$⊢ v \in V$
39		vex	$⊢ e \in V$
40	38 39	op2ndd	$⊢ b = ⟨v, e⟩ \to 2^{nd} (b) = e$
41	40	adantr	$⊢ (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to 2^{nd} (b) = e$
42	41	adantr	$⊢ ((b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \land (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))) \to 2^{nd} (b) = e$
43	37 42	eqeq12d	$⊢ ((b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \land (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))) \to (2^{nd} (a) = 2^{nd} (b) \leftrightarrow f = e)$
44		eqeq12	$⊢ (a = ⟨w, f⟩ \land b = ⟨v, e⟩) \to (a = b \leftrightarrow ⟨w, f⟩ = ⟨v, e⟩)$
45	44	ex	$⊢ a = ⟨w, f⟩ \to (b = ⟨v, e⟩ \to (a = b \leftrightarrow ⟨w, f⟩ = ⟨v, e⟩))$
46	45	adantr	$⊢ (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (b = ⟨v, e⟩ \to (a = b \leftrightarrow ⟨w, f⟩ = ⟨v, e⟩))$
47	46	com12	$⊢ b = ⟨v, e⟩ \to ((a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (a = b \leftrightarrow ⟨w, f⟩ = ⟨v, e⟩))$
48	47	adantr	$⊢ (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to ((a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (a = b \leftrightarrow ⟨w, f⟩ = ⟨v, e⟩))$
49	48	imp	$⊢ ((b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \land (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))) \to (a = b \leftrightarrow ⟨w, f⟩ = ⟨v, e⟩)$
50	33 43 49	3imtr4d	$⊢ ((b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \land (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f)))) \to (2^{nd} (a) = 2^{nd} (b) \to a = b)$
51	50	ex	$⊢ (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to ((a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (2^{nd} (a) = 2^{nd} (b) \to a = b))$
52	51	exlimivv	$⊢ \exists v \exists e (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to ((a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (2^{nd} (a) = 2^{nd} (b) \to a = b))$
53	52	com12	$⊢ (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (\exists v \exists e (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to (2^{nd} (a) = 2^{nd} (b) \to a = b))$
54	53	exlimivv	$⊢ \exists w \exists f (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \to (\exists v \exists e (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e))) \to (2^{nd} (a) = 2^{nd} (b) \to a = b))$
55	54	imp	$⊢ (\exists w \exists f (a = ⟨w, f⟩ \land (w = V \land \exists q \in USHGraph (Vtx (q) = w \land Edg (q) = f))) \land \exists v \exists e (b = ⟨v, e⟩ \land (v = V \land \exists q \in USHGraph (Vtx (q) = v \land Edg (q) = e)))) \to (2^{nd} (a) = 2^{nd} (b) \to a = b)$
56	21 24 55	syl2anb	$⊢ (a \in G \land b \in G) \to (2^{nd} (a) = 2^{nd} (b) \to a = b)$
57	7 56	sylbid	$⊢ (a \in G \land b \in G) \to (F (a) = F (b) \to a = b)$
58	57	rgen2	$⊢ \forall a \in G \forall b \in G (F (a) = F (b) \to a = b)$
59		dff13	$⊢ F : G \underset{1-1}{⟶} P \leftrightarrow (F : G ⟶ P \land \forall a \in G \forall b \in G (F (a) = F (b) \to a = b))$
60	4 58 59	mpbir2an	$⊢ F : G \underset{1-1}{⟶} P$

Metamath Proof Explorer

Theorem uspgrsprf1

Proof