Proof of Theorem uspgrsprf
Step | Hyp | Ref
| Expression |
1 | | uspgrsprf.f |
. 2
⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔)) |
2 | | uspgrsprf.g |
. . . . 5
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} |
3 | 2 | eleq2i 2824 |
. . . 4
⊢ (𝑔 ∈ 𝐺 ↔ 𝑔 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}) |
4 | | elopab 5382 |
. . . 4
⊢ (𝑔 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} ↔ ∃𝑣∃𝑒(𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) |
5 | 3, 4 | bitri 278 |
. . 3
⊢ (𝑔 ∈ 𝐺 ↔ ∃𝑣∃𝑒(𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) |
6 | | uspgrupgr 27121 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ USPGraph → 𝑞 ∈
UPGraph) |
7 | | upgredgssspr 44839 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ UPGraph →
(Edg‘𝑞) ⊆
(Pairs‘(Vtx‘𝑞))) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ USPGraph →
(Edg‘𝑞) ⊆
(Pairs‘(Vtx‘𝑞))) |
9 | 8 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ USPGraph ∧
((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → (Edg‘𝑞) ⊆ (Pairs‘(Vtx‘𝑞))) |
10 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → (Edg‘𝑞) = 𝑒) |
11 | | fveq2 6674 |
. . . . . . . . . . . . . 14
⊢
((Vtx‘𝑞) =
𝑣 →
(Pairs‘(Vtx‘𝑞))
= (Pairs‘𝑣)) |
12 | 11 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → (Pairs‘(Vtx‘𝑞)) = (Pairs‘𝑣)) |
13 | 10, 12 | sseq12d 3910 |
. . . . . . . . . . . 12
⊢
(((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → ((Edg‘𝑞) ⊆ (Pairs‘(Vtx‘𝑞)) ↔ 𝑒 ⊆ (Pairs‘𝑣))) |
14 | 13 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ USPGraph ∧
((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → ((Edg‘𝑞) ⊆ (Pairs‘(Vtx‘𝑞)) ↔ 𝑒 ⊆ (Pairs‘𝑣))) |
15 | 9, 14 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ USPGraph ∧
((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → 𝑒 ⊆ (Pairs‘𝑣)) |
16 | 15 | rexlimiva 3191 |
. . . . . . . . 9
⊢
(∃𝑞 ∈
USPGraph ((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → 𝑒 ⊆ (Pairs‘𝑣)) |
17 | 16 | adantl 485 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → 𝑒 ⊆ (Pairs‘𝑣)) |
18 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑉 → (Pairs‘𝑣) = (Pairs‘𝑉)) |
19 | 18 | sseq2d 3909 |
. . . . . . . . 9
⊢ (𝑣 = 𝑉 → (𝑒 ⊆ (Pairs‘𝑣) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
20 | 19 | adantr 484 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → (𝑒 ⊆ (Pairs‘𝑣) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
21 | 17, 20 | mpbid 235 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → 𝑒 ⊆ (Pairs‘𝑉)) |
22 | 21 | adantl 485 |
. . . . . 6
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → 𝑒 ⊆ (Pairs‘𝑉)) |
23 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
24 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑒 ∈ V |
25 | 23, 24 | op2ndd 7725 |
. . . . . . . 8
⊢ (𝑔 = 〈𝑣, 𝑒〉 → (2nd ‘𝑔) = 𝑒) |
26 | 25 | sseq1d 3908 |
. . . . . . 7
⊢ (𝑔 = 〈𝑣, 𝑒〉 → ((2nd ‘𝑔) ⊆ (Pairs‘𝑉) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
27 | 26 | adantr 484 |
. . . . . 6
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((2nd ‘𝑔) ⊆ (Pairs‘𝑉) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
28 | 22, 27 | mpbird 260 |
. . . . 5
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑔) ⊆ (Pairs‘𝑉)) |
29 | | uspgrsprf.p |
. . . . . . 7
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) |
30 | 29 | eleq2i 2824 |
. . . . . 6
⊢
((2nd ‘𝑔) ∈ 𝑃 ↔ (2nd ‘𝑔) ∈ 𝒫
(Pairs‘𝑉)) |
31 | | fvex 6687 |
. . . . . . 7
⊢
(2nd ‘𝑔) ∈ V |
32 | 31 | elpw 4492 |
. . . . . 6
⊢
((2nd ‘𝑔) ∈ 𝒫 (Pairs‘𝑉) ↔ (2nd
‘𝑔) ⊆
(Pairs‘𝑉)) |
33 | 30, 32 | bitri 278 |
. . . . 5
⊢
((2nd ‘𝑔) ∈ 𝑃 ↔ (2nd ‘𝑔) ⊆ (Pairs‘𝑉)) |
34 | 28, 33 | sylibr 237 |
. . . 4
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑔) ∈ 𝑃) |
35 | 34 | exlimivv 1939 |
. . 3
⊢
(∃𝑣∃𝑒(𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑔) ∈ 𝑃) |
36 | 5, 35 | sylbi 220 |
. 2
⊢ (𝑔 ∈ 𝐺 → (2nd ‘𝑔) ∈ 𝑃) |
37 | 1, 36 | fmpti 6886 |
1
⊢ 𝐹:𝐺⟶𝑃 |