Theorem 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	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
	uspgrsprf.f	⊢ 𝐹 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
Assertion	uspgrsprf	⊢ 𝐹 : 𝐺 ⟶ 𝑃

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3		uspgrsprf.f	⊢ 𝐹 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
4	2	eleq2i	⊢ ( 𝑔 ∈ 𝐺 ↔ 𝑔 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } )
5		elopab	⊢ ( 𝑔 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } ↔ ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) )
6	4 5	bitri	⊢ ( 𝑔 ∈ 𝐺 ↔ ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) )
7		uspgrupgr	⊢ ( 𝑞 ∈ USPGraph → 𝑞 ∈ UPGraph )
8		upgredgssspr	⊢ ( 𝑞 ∈ UPGraph → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) )
9	7 8	syl	⊢ ( 𝑞 ∈ USPGraph → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) )
10	9	adantr	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) )
11		simpr	⊢ ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → ( Edg ‘ 𝑞 ) = 𝑒 )
12		fveq2	⊢ ( ( Vtx ‘ 𝑞 ) = 𝑣 → ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) = ( Pairs ‘ 𝑣 ) )
13	12	adantr	⊢ ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) = ( Pairs ‘ 𝑣 ) )
14	11 13	sseq12d	⊢ ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → ( ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) ↔ 𝑒 ⊆ ( Pairs ‘ 𝑣 ) ) )
15	14	adantl	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → ( ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) ↔ 𝑒 ⊆ ( Pairs ‘ 𝑣 ) ) )
16	10 15	mpbid	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → 𝑒 ⊆ ( Pairs ‘ 𝑣 ) )
17	16	rexlimiva	⊢ ( ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → 𝑒 ⊆ ( Pairs ‘ 𝑣 ) )
18	17	adantl	⊢ ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → 𝑒 ⊆ ( Pairs ‘ 𝑣 ) )
19		fveq2	⊢ ( 𝑣 = 𝑉 → ( Pairs ‘ 𝑣 ) = ( Pairs ‘ 𝑉 ) )
20	19	sseq2d	⊢ ( 𝑣 = 𝑉 → ( 𝑒 ⊆ ( Pairs ‘ 𝑣 ) ↔ 𝑒 ⊆ ( Pairs ‘ 𝑉 ) ) )
21	20	adantr	⊢ ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → ( 𝑒 ⊆ ( Pairs ‘ 𝑣 ) ↔ 𝑒 ⊆ ( Pairs ‘ 𝑉 ) ) )
22	18 21	mpbid	⊢ ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → 𝑒 ⊆ ( Pairs ‘ 𝑉 ) )
23	22	adantl	⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → 𝑒 ⊆ ( Pairs ‘ 𝑉 ) )
24		vex	⊢ 𝑣 ∈ V
25		vex	⊢ 𝑒 ∈ V
26	24 25	op2ndd	⊢ ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ → ( 2nd ‘ 𝑔 ) = 𝑒 )
27	26	sseq1d	⊢ ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ → ( ( 2nd ‘ 𝑔 ) ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑒 ⊆ ( Pairs ‘ 𝑉 ) ) )
28	27	adantr	⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 2nd ‘ 𝑔 ) ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑒 ⊆ ( Pairs ‘ 𝑉 ) ) )
29	23 28	mpbird	⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( 2nd ‘ 𝑔 ) ⊆ ( Pairs ‘ 𝑉 ) )
30	1	eleq2i	⊢ ( ( 2nd ‘ 𝑔 ) ∈ 𝑃 ↔ ( 2nd ‘ 𝑔 ) ∈ 𝒫 ( Pairs ‘ 𝑉 ) )
31		fvex	⊢ ( 2nd ‘ 𝑔 ) ∈ V
32	31	elpw	⊢ ( ( 2nd ‘ 𝑔 ) ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↔ ( 2nd ‘ 𝑔 ) ⊆ ( Pairs ‘ 𝑉 ) )
33	30 32	bitri	⊢ ( ( 2nd ‘ 𝑔 ) ∈ 𝑃 ↔ ( 2nd ‘ 𝑔 ) ⊆ ( Pairs ‘ 𝑉 ) )
34	29 33	sylibr	⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( 2nd ‘ 𝑔 ) ∈ 𝑃 )
35	34	exlimivv	⊢ ( ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( 2nd ‘ 𝑔 ) ∈ 𝑃 )
36	6 35	sylbi	⊢ ( 𝑔 ∈ 𝐺 → ( 2nd ‘ 𝑔 ) ∈ 𝑃 )
37	3 36	fmpti	⊢ 𝐹 : 𝐺 ⟶ 𝑃