Proof of Theorem uhgrstrrepe
Step | Hyp | Ref
| Expression |
1 | | uhgrstrrepe.e |
. . . 4
⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) |
2 | | uhgrstrrepe.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝐺) |
3 | | baseid 15747 |
. . . . . . . . . 10
⊢ Base =
Slot (Base‘ndx) |
4 | | slotsbaseefdif 25672 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (.ef‘ndx) |
5 | | uhgrstrrepe.i |
. . . . . . . . . . 11
⊢ 𝐼 =
(.ef‘ndx) |
6 | 4, 5 | neeqtrri 2855 |
. . . . . . . . . 10
⊢
(Base‘ndx) ≠ 𝐼 |
7 | 3, 6 | setsnid 15743 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘(𝐺 sSet
〈𝐼, 𝐸〉)) |
8 | | uhgrstrrepe.s |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Struct 〈(Base‘ndx), 𝐼〉) |
9 | | uhgrstrrepe.b |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘ndx) ∈
dom 𝐺) |
10 | | uhgrstrrepe.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ 𝑈) |
11 | | uhgrstrrepe.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ 𝑊) |
12 | 2, 5, 8, 9, 10, 1,
11 | uhgrstrrepelem 25744 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 sSet 〈𝐼, 𝐸〉) ∈ V ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧
{(Base‘ndx), (.ef‘ndx)} ⊆ dom (𝐺 sSet 〈𝐼, 𝐸〉))) |
13 | | funvtxval 25695 |
. . . . . . . . . . 11
⊢ (((𝐺 sSet 〈𝐼, 𝐸〉) ∈ V ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧
{(Base‘ndx), (.ef‘ndx)} ⊆ dom (𝐺 sSet 〈𝐼, 𝐸〉)) → (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (Base‘(𝐺 sSet 〈𝐼, 𝐸〉))) |
14 | 13 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (((𝐺 sSet 〈𝐼, 𝐸〉) ∈ V ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧
{(Base‘ndx), (.ef‘ndx)} ⊆ dom (𝐺 sSet 〈𝐼, 𝐸〉)) → (Base‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉))) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉))) |
16 | 7, 15 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐺) = (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉))) |
17 | 2, 16 | syl5req 2657 |
. . . . . . 7
⊢ (𝜑 → (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) = 𝑉) |
18 | 17 | pweqd 4113 |
. . . . . 6
⊢ (𝜑 → 𝒫
(Vtx‘(𝐺 sSet
〈𝐼, 𝐸〉)) = 𝒫 𝑉) |
19 | 18 | difeq1d 3689 |
. . . . 5
⊢ (𝜑 → (𝒫
(Vtx‘(𝐺 sSet
〈𝐼, 𝐸〉)) ∖ {∅}) = (𝒫
𝑉 ∖
{∅})) |
20 | 19 | feq3d 5945 |
. . . 4
⊢ (𝜑 → (𝐸:dom 𝐸⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖ {∅}) ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
21 | 1, 20 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖
{∅})) |
22 | 5 | opeq1i 4343 |
. . . . . . 7
⊢
〈𝐼, 𝐸〉 = 〈(.ef‘ndx),
𝐸〉 |
23 | 22 | oveq2i 6560 |
. . . . . 6
⊢ (𝐺 sSet 〈𝐼, 𝐸〉) = (𝐺 sSet 〈(.ef‘ndx), 𝐸〉) |
24 | 23 | fveq2i 6106 |
. . . . 5
⊢
(.ef‘(𝐺 sSet
〈𝐼, 𝐸〉)) = (.ef‘(𝐺 sSet 〈(.ef‘ndx), 𝐸〉)) |
25 | | funiedgval 25696 |
. . . . . 6
⊢ (((𝐺 sSet 〈𝐼, 𝐸〉) ∈ V ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧
{(Base‘ndx), (.ef‘ndx)} ⊆ dom (𝐺 sSet 〈𝐼, 𝐸〉)) → (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (.ef‘(𝐺 sSet 〈𝐼, 𝐸〉))) |
26 | 12, 25 | syl 17 |
. . . . 5
⊢ (𝜑 → (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (.ef‘(𝐺 sSet 〈𝐼, 𝐸〉))) |
27 | | df-edgf 25668 |
. . . . . . . 8
⊢ .ef =
Slot ;18 |
28 | | 1nn0 11185 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
29 | | 8nn 11068 |
. . . . . . . . 9
⊢ 8 ∈
ℕ |
30 | 28, 29 | decnncl 11394 |
. . . . . . . 8
⊢ ;18 ∈ ℕ |
31 | 27, 30 | ndxid 15716 |
. . . . . . 7
⊢ .ef =
Slot (.ef‘ndx) |
32 | 31 | setsid 15742 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → 𝐸 = (.ef‘(𝐺 sSet 〈(.ef‘ndx), 𝐸〉))) |
33 | 10, 11, 32 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝐸 = (.ef‘(𝐺 sSet 〈(.ef‘ndx), 𝐸〉))) |
34 | 24, 26, 33 | 3eqtr4a 2670 |
. . . 4
⊢ (𝜑 → (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) = 𝐸) |
35 | 34 | dmeqd 5248 |
. . . 4
⊢ (𝜑 → dom (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) = dom 𝐸) |
36 | 34, 35 | feq12d 5946 |
. . 3
⊢ (𝜑 → ((iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)):dom (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉))⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖ {∅}) ↔ 𝐸:dom 𝐸⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖
{∅}))) |
37 | 21, 36 | mpbird 246 |
. 2
⊢ (𝜑 → (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)):dom (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉))⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖
{∅})) |
38 | | ovex 6577 |
. . 3
⊢ (𝐺 sSet 〈𝐼, 𝐸〉) ∈ V |
39 | | eqid 2610 |
. . . 4
⊢
(Vtx‘(𝐺 sSet
〈𝐼, 𝐸〉)) = (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) |
40 | | eqid 2610 |
. . . 4
⊢
(iEdg‘(𝐺 sSet
〈𝐼, 𝐸〉)) = (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) |
41 | 39, 40 | isuhgr 25726 |
. . 3
⊢ ((𝐺 sSet 〈𝐼, 𝐸〉) ∈ V → ((𝐺 sSet 〈𝐼, 𝐸〉) ∈ UHGraph ↔
(iEdg‘(𝐺 sSet
〈𝐼, 𝐸〉)):dom (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉))⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖
{∅}))) |
42 | 38, 41 | mp1i 13 |
. 2
⊢ (𝜑 → ((𝐺 sSet 〈𝐼, 𝐸〉) ∈ UHGraph ↔
(iEdg‘(𝐺 sSet
〈𝐼, 𝐸〉)):dom (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉))⟶(𝒫 (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) ∖
{∅}))) |
43 | 37, 42 | mpbird 246 |
1
⊢ (𝜑 → (𝐺 sSet 〈𝐼, 𝐸〉) ∈ UHGraph ) |