Proof of Theorem uspgrsprf
Step | Hyp | Ref
| Expression |
1 | | uspgrsprf.f |
. 2
⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔)) |
2 | | uspgrsprf.g |
. . . . 5
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} |
3 | 2 | eleq2i 2830 |
. . . 4
⊢ (𝑔 ∈ 𝐺 ↔ 𝑔 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}) |
4 | | elopab 5440 |
. . . 4
⊢ (𝑔 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} ↔ ∃𝑣∃𝑒(𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) |
5 | 3, 4 | bitri 274 |
. . 3
⊢ (𝑔 ∈ 𝐺 ↔ ∃𝑣∃𝑒(𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) |
6 | | uspgrupgr 27546 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ USPGraph → 𝑞 ∈
UPGraph) |
7 | | upgredgssspr 45305 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ UPGraph →
(Edg‘𝑞) ⊆
(Pairs‘(Vtx‘𝑞))) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ USPGraph →
(Edg‘𝑞) ⊆
(Pairs‘(Vtx‘𝑞))) |
9 | 8 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ USPGraph ∧
((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → (Edg‘𝑞) ⊆ (Pairs‘(Vtx‘𝑞))) |
10 | | simpr 485 |
. . . . . . . . . . . . 13
⊢
(((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → (Edg‘𝑞) = 𝑒) |
11 | | fveq2 6774 |
. . . . . . . . . . . . . 14
⊢
((Vtx‘𝑞) =
𝑣 →
(Pairs‘(Vtx‘𝑞))
= (Pairs‘𝑣)) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → (Pairs‘(Vtx‘𝑞)) = (Pairs‘𝑣)) |
13 | 10, 12 | sseq12d 3954 |
. . . . . . . . . . . 12
⊢
(((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → ((Edg‘𝑞) ⊆ (Pairs‘(Vtx‘𝑞)) ↔ 𝑒 ⊆ (Pairs‘𝑣))) |
14 | 13 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ USPGraph ∧
((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → ((Edg‘𝑞) ⊆ (Pairs‘(Vtx‘𝑞)) ↔ 𝑒 ⊆ (Pairs‘𝑣))) |
15 | 9, 14 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ USPGraph ∧
((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → 𝑒 ⊆ (Pairs‘𝑣)) |
16 | 15 | rexlimiva 3210 |
. . . . . . . . 9
⊢
(∃𝑞 ∈
USPGraph ((Vtx‘𝑞) =
𝑣 ∧ (Edg‘𝑞) = 𝑒) → 𝑒 ⊆ (Pairs‘𝑣)) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → 𝑒 ⊆ (Pairs‘𝑣)) |
18 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑉 → (Pairs‘𝑣) = (Pairs‘𝑉)) |
19 | 18 | sseq2d 3953 |
. . . . . . . . 9
⊢ (𝑣 = 𝑉 → (𝑒 ⊆ (Pairs‘𝑣) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
20 | 19 | adantr 481 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → (𝑒 ⊆ (Pairs‘𝑣) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
21 | 17, 20 | mpbid 231 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) → 𝑒 ⊆ (Pairs‘𝑉)) |
22 | 21 | adantl 482 |
. . . . . 6
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → 𝑒 ⊆ (Pairs‘𝑉)) |
23 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
24 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑒 ∈ V |
25 | 23, 24 | op2ndd 7842 |
. . . . . . . 8
⊢ (𝑔 = 〈𝑣, 𝑒〉 → (2nd ‘𝑔) = 𝑒) |
26 | 25 | sseq1d 3952 |
. . . . . . 7
⊢ (𝑔 = 〈𝑣, 𝑒〉 → ((2nd ‘𝑔) ⊆ (Pairs‘𝑉) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
27 | 26 | adantr 481 |
. . . . . 6
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((2nd ‘𝑔) ⊆ (Pairs‘𝑉) ↔ 𝑒 ⊆ (Pairs‘𝑉))) |
28 | 22, 27 | mpbird 256 |
. . . . 5
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑔) ⊆ (Pairs‘𝑉)) |
29 | | uspgrsprf.p |
. . . . . . 7
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) |
30 | 29 | eleq2i 2830 |
. . . . . 6
⊢
((2nd ‘𝑔) ∈ 𝑃 ↔ (2nd ‘𝑔) ∈ 𝒫
(Pairs‘𝑉)) |
31 | | fvex 6787 |
. . . . . . 7
⊢
(2nd ‘𝑔) ∈ V |
32 | 31 | elpw 4537 |
. . . . . 6
⊢
((2nd ‘𝑔) ∈ 𝒫 (Pairs‘𝑉) ↔ (2nd
‘𝑔) ⊆
(Pairs‘𝑉)) |
33 | 30, 32 | bitri 274 |
. . . . 5
⊢
((2nd ‘𝑔) ∈ 𝑃 ↔ (2nd ‘𝑔) ⊆ (Pairs‘𝑉)) |
34 | 28, 33 | sylibr 233 |
. . . 4
⊢ ((𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑔) ∈ 𝑃) |
35 | 34 | exlimivv 1935 |
. . 3
⊢
(∃𝑣∃𝑒(𝑔 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑔) ∈ 𝑃) |
36 | 5, 35 | sylbi 216 |
. 2
⊢ (𝑔 ∈ 𝐺 → (2nd ‘𝑔) ∈ 𝑃) |
37 | 1, 36 | fmpti 6986 |
1
⊢ 𝐹:𝐺⟶𝑃 |