Metamath Proof Explorer

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 ⊢ P = 𝒫 Pairs ⁡ V
uspgrsprf.g ⊢ G = v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
uspgrsprf.f ⊢ F = g ∈ 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 ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
3 uspgrsprf.f ⊢ F = g ∈ G ⟼ 2 nd ⁡ g
4 2 eleq2i ⊢ g ∈ G ↔ g ∈ v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
5 elopab ⊢ g ∈ v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e ↔ ∃ v ∃ e g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
6 4 5 bitri ⊢ g ∈ G ↔ ∃ v ∃ e g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
7 uspgrupgr ⊢ q ∈ USHGraph → q ∈ UPGraph
8 upgredgssspr ⊢ q ∈ UPGraph → Edg ⁡ q ⊆ Pairs ⁡ Vtx ⁡ q
9 7 8 syl ⊢ q ∈ USHGraph → Edg ⁡ q ⊆ Pairs ⁡ Vtx ⁡ q
10 9 adantr ⊢ q ∈ USHGraph ∧ Vtx ⁡ q = v ∧ Edg ⁡ q = e → Edg ⁡ q ⊆ Pairs ⁡ Vtx ⁡ q
11 simpr ⊢ Vtx ⁡ q = v ∧ Edg ⁡ q = e → Edg ⁡ q = e
12 fveq2 ⊢ Vtx ⁡ q = v → Pairs ⁡ Vtx ⁡ q = Pairs ⁡ v
13 12 adantr ⊢ Vtx ⁡ q = v ∧ Edg ⁡ q = e → Pairs ⁡ Vtx ⁡ q = Pairs ⁡ v
14 11 13 sseq12d ⊢ Vtx ⁡ q = v ∧ Edg ⁡ q = e → Edg ⁡ q ⊆ Pairs ⁡ Vtx ⁡ q ↔ e ⊆ Pairs ⁡ v
15 14 adantl ⊢ q ∈ USHGraph ∧ Vtx ⁡ q = v ∧ Edg ⁡ q = e → Edg ⁡ q ⊆ Pairs ⁡ Vtx ⁡ q ↔ e ⊆ Pairs ⁡ v
16 10 15 mpbid ⊢ q ∈ USHGraph ∧ Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ⊆ Pairs ⁡ v
17 16 rexlimiva ⊢ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ⊆ Pairs ⁡ v
18 17 adantl ⊢ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ⊆ Pairs ⁡ v
19 fveq2 ⊢ v = V → Pairs ⁡ v = Pairs ⁡ V
20 19 sseq2d ⊢ v = V → e ⊆ Pairs ⁡ v ↔ e ⊆ Pairs ⁡ V
21 20 adantr ⊢ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ⊆ Pairs ⁡ v ↔ e ⊆ Pairs ⁡ V
22 18 21 mpbid ⊢ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ⊆ Pairs ⁡ V
23 22 adantl ⊢ g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ⊆ Pairs ⁡ V
24 vex ⊢ v ∈ V
25 vex ⊢ e ∈ V
26 24 25 op2ndd ⊢ g = v e → 2 nd ⁡ g = e
27 26 sseq1d ⊢ g = v e → 2 nd ⁡ g ⊆ Pairs ⁡ V ↔ e ⊆ Pairs ⁡ V
28 27 adantr ⊢ g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → 2 nd ⁡ g ⊆ Pairs ⁡ V ↔ e ⊆ Pairs ⁡ V
29 23 28 mpbird ⊢ g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → 2 nd ⁡ g ⊆ Pairs ⁡ V
30 1 eleq2i ⊢ 2 nd ⁡ g ∈ P ↔ 2 nd ⁡ g ∈ 𝒫 Pairs ⁡ V
31 fvex ⊢ 2 nd ⁡ g ∈ V
32 31 elpw ⊢ 2 nd ⁡ g ∈ 𝒫 Pairs ⁡ V ↔ 2 nd ⁡ g ⊆ Pairs ⁡ V
33 30 32 bitri ⊢ 2 nd ⁡ g ∈ P ↔ 2 nd ⁡ g ⊆ Pairs ⁡ V
34 29 33 sylibr ⊢ g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → 2 nd ⁡ g ∈ P
35 34 exlimivv ⊢ ∃ v ∃ e g = v e ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → 2 nd ⁡ g ∈ P
36 6 35 sylbi ⊢ g ∈ G → 2 nd ⁡ g ∈ P
37 3 36 fmpti ⊢ F : G ⟶ P