Step | Hyp | Ref
| Expression |
1 | | isubgr3stgr.n |
. . . 4
⊢ 𝑁 ∈
ℕ0 |
2 | | stgredgel 47859 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐽 ∈
(Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦}))) |
3 | 1, 2 | mp1i 13 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦}))) |
4 | | c0ex 11252 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
5 | 4 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V) |
6 | | prssg 4823 |
. . . . . . . . . . . 12
⊢ ((0
∈ V ∧ 𝑦 ∈
(1...𝑁)) → ((0 ∈
(0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁))) |
7 | 5, 6 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁))) |
8 | | f1ocnv 6860 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐶–1-1-onto→𝑊 → ◡𝐹:𝑊–1-1-onto→𝐶) |
9 | | f1ofn 6849 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:𝑊–1-1-onto→𝐶 → ◡𝐹 Fn 𝑊) |
10 | | isubgr3stgr.w |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑊 = (Vtx‘𝑆) |
11 | | isubgr3stgr.s |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑆 = (StarGr‘𝑁) |
12 | 11 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Vtx‘𝑆) =
(Vtx‘(StarGr‘𝑁)) |
13 | | stgrvtx 47856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) |
14 | 1, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Vtx‘(StarGr‘𝑁)) = (0...𝑁) |
15 | 10, 12, 14 | 3eqtri 2766 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑊 = (0...𝑁) |
16 | 15 | fneq2i 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹 Fn 𝑊 ↔ ◡𝐹 Fn (0...𝑁)) |
17 | 9, 16 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹:𝑊–1-1-onto→𝐶 → ◡𝐹 Fn (0...𝑁)) |
18 | 8, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐶–1-1-onto→𝑊 → ◡𝐹 Fn (0...𝑁)) |
19 | 18 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ◡𝐹 Fn (0...𝑁)) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ◡𝐹 Fn (0...𝑁)) |
21 | 20 | anim1i 615 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))) |
22 | | 3anass 1094 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ (◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))) |
23 | 21, 22 | sylibr 234 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) |
24 | 23 | ex 412 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) → (◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))) |
25 | 7, 24 | sylbird 260 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({0, 𝑦} ⊆ (0...𝑁) → (◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))) |
26 | 25 | imp 406 |
. . . . . . . . 9
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) |
27 | | fnimapr 6991 |
. . . . . . . . 9
⊢ ((◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) → (◡𝐹 “ {0, 𝑦}) = {(◡𝐹‘0), (◡𝐹‘𝑦)}) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (◡𝐹 “ {0, 𝑦}) = {(◡𝐹‘0), (◡𝐹‘𝑦)}) |
29 | | isubgr3stgr.v |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑉 = (Vtx‘𝐺) |
30 | 29 | clnbgrvtxel 47753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋)) |
32 | | isubgr3stgr.c |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) |
33 | 31, 32 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝐶) |
34 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐹:𝐶–1-1-onto→𝑊) |
35 | 33, 34 | anim12ci 614 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶)) |
36 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹‘𝑋) = 0) |
37 | 35, 36 | jca 511 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0)) |
39 | | f1ocnvfv 7297 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) → ((𝐹‘𝑋) = 0 → (◡𝐹‘0) = 𝑋)) |
40 | 39 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0) → (◡𝐹‘0) = 𝑋) |
41 | 38, 40 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (◡𝐹‘0) = 𝑋) |
42 | 30, 32 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐶) |
43 | 42 | ad3antlr 731 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑋 ∈ 𝐶) |
44 | | f1of 6848 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:𝑊–1-1-onto→𝐶 → ◡𝐹:𝑊⟶𝐶) |
45 | 8, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐶–1-1-onto→𝑊 → ◡𝐹:𝑊⟶𝐶) |
46 | 45 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ◡𝐹:𝑊⟶𝐶) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ◡𝐹:𝑊⟶𝐶) |
48 | | fz1ssfz0 13659 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑁) ⊆
(0...𝑁) |
49 | 48 | sseli 3990 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ (0...𝑁)) |
50 | 49, 15 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ 𝑊) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑦 ∈ 𝑊) |
52 | 47, 51 | ffvelcdmd 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (◡𝐹‘𝑦) ∈ 𝐶) |
53 | 43, 52 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑋 ∈ 𝐶 ∧ (◡𝐹‘𝑦) ∈ 𝐶)) |
54 | 32 | eleq2i 2830 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹‘𝑦) ∈ 𝐶 ↔ (◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋)) |
55 | | usgrupgr 29216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UPGraph) |
56 | 55 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉)) |
57 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉)) |
58 | 29 | clnbgrssvtx 47755 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉 |
59 | 32, 58 | eqsstri 4029 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐶 ⊆ 𝑉 |
60 | 59, 52 | sselid 3992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (◡𝐹‘𝑦) ∈ 𝑉) |
61 | | df-3an 1088 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑦) ∈ 𝑉) ↔ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉) ∧ (◡𝐹‘𝑦) ∈ 𝑉)) |
62 | 57, 60, 61 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑦) ∈ 𝑉)) |
63 | 62 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑦) ∈ 𝑉)) |
64 | | isubgr3stgr.e |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐸 = (Edg‘𝐺) |
65 | 29, 64 | clnbupgrel 47758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑦) ∈ 𝑉) → ((◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((◡𝐹‘𝑦) = 𝑋 ∨ {(◡𝐹‘𝑦), 𝑋} ∈ 𝐸))) |
66 | 63, 65 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((◡𝐹‘𝑦) = 𝑋 ∨ {(◡𝐹‘𝑦), 𝑋} ∈ 𝐸))) |
67 | 54, 66 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((◡𝐹‘𝑦) ∈ 𝐶 ↔ ((◡𝐹‘𝑦) = 𝑋 ∨ {(◡𝐹‘𝑦), 𝑋} ∈ 𝐸))) |
68 | | eqeq2 2746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝐹‘0) = 𝑋 → ((◡𝐹‘𝑦) = (◡𝐹‘0) ↔ (◡𝐹‘𝑦) = 𝑋)) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) → ((◡𝐹‘𝑦) = (◡𝐹‘0) ↔ (◡𝐹‘𝑦) = 𝑋)) |
70 | | f1of1 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡𝐹:𝑊–1-1-onto→𝐶 → ◡𝐹:𝑊–1-1→𝐶) |
71 | 8, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝐶–1-1-onto→𝑊 → ◡𝐹:𝑊–1-1→𝐶) |
72 | 71 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ◡𝐹:𝑊–1-1→𝐶) |
73 | | 0elfz 13660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
74 | 1, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
(0...𝑁) |
75 | 74, 15 | eleqtrri 2837 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
𝑊 |
76 | 50, 75 | jctir 520 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (1...𝑁) → (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) |
77 | | f1veqaeq 7276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡𝐹:𝑊–1-1→𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((◡𝐹‘𝑦) = (◡𝐹‘0) → 𝑦 = 0)) |
78 | 72, 76, 77 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((◡𝐹‘𝑦) = (◡𝐹‘0) → 𝑦 = 0)) |
79 | | elfznn 13589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ) |
80 | | nnne0 12297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
81 | | eqneqall 2948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 0 → (𝑦 ≠ 0 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
82 | 80, 81 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → (𝑦 = 0 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
83 | 79, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (1...𝑁) → (𝑦 = 0 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑦 = 0 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
85 | 78, 84 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((◡𝐹‘𝑦) = (◡𝐹‘0) → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) → ((◡𝐹‘𝑦) = (◡𝐹‘0) → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
87 | 69, 86 | sylbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) → ((◡𝐹‘𝑦) = 𝑋 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((◡𝐹‘𝑦) = 𝑋 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
89 | | prcom 4736 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {(◡𝐹‘𝑦), 𝑋} = {𝑋, (◡𝐹‘𝑦)} |
90 | 89 | eleq1i 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({(◡𝐹‘𝑦), 𝑋} ∈ 𝐸 ↔ {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸) |
91 | 90 | biimpi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ ({(◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ({(◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
93 | 88, 92 | jaod 859 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (((◡𝐹‘𝑦) = 𝑋 ∨ {(◡𝐹‘𝑦), 𝑋} ∈ 𝐸) → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
94 | 67, 93 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((◡𝐹‘𝑦) ∈ 𝐶 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
95 | 94 | impr 454 |
. . . . . . . . . . . . . 14
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (◡𝐹‘𝑦) ∈ 𝐶)) → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸) |
96 | | prssi 4825 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝐶 ∧ (◡𝐹‘𝑦) ∈ 𝐶) → {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (◡𝐹‘𝑦) ∈ 𝐶)) → {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶) |
98 | 95, 97 | jca 511 |
. . . . . . . . . . . . 13
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (◡𝐹‘𝑦) ∈ 𝐶)) → ({𝑋, (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶)) |
99 | 53, 98 | mpidan 689 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) → ({𝑋, (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶)) |
100 | | preq1 4737 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹‘0) = 𝑋 → {(◡𝐹‘0), (◡𝐹‘𝑦)} = {𝑋, (◡𝐹‘𝑦)}) |
101 | 100 | eleq1d 2823 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹‘0) = 𝑋 → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
102 | 100 | sseq1d 4026 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹‘0) = 𝑋 → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶 ↔ {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶)) |
103 | 101, 102 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹‘0) = 𝑋 → (({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶) ↔ ({𝑋, (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶))) |
104 | 103 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) → (({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶) ↔ ({𝑋, (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (◡𝐹‘𝑦)} ⊆ 𝐶))) |
105 | 99, 104 | mpbird 257 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶)) |
106 | 41, 105 | mpdan 687 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶)) |
107 | 106 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶)) |
108 | | usgruhgr 29217 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UHGraph) |
109 | 108 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝐺 ∈ UHGraph) |
110 | 59 | a1i 11 |
. . . . . . . . . 10
⊢ ({0,
𝑦} ⊆ (0...𝑁) → 𝐶 ⊆ 𝑉) |
111 | | eqid 2734 |
. . . . . . . . . . 11
⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶) |
112 | | isubgr3stgr.i |
. . . . . . . . . . 11
⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) |
113 | 29, 64, 111, 112 | isubgredg 47789 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉) → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶))) |
114 | 109, 110,
113 | syl2an 596 |
. . . . . . . . 9
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(◡𝐹‘0), (◡𝐹‘𝑦)} ⊆ 𝐶))) |
115 | 107, 114 | mpbird 257 |
. . . . . . . 8
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → {(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐼) |
116 | 28, 115 | eqeltrd 2838 |
. . . . . . 7
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (◡𝐹 “ {0, 𝑦}) ∈ 𝐼) |
117 | 116 | ex 412 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({0, 𝑦} ⊆ (0...𝑁) → (◡𝐹 “ {0, 𝑦}) ∈ 𝐼)) |
118 | | sseq1 4020 |
. . . . . . 7
⊢ (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) ↔ {0, 𝑦} ⊆ (0...𝑁))) |
119 | | imaeq2 6075 |
. . . . . . . 8
⊢ (𝐽 = {0, 𝑦} → (◡𝐹 “ 𝐽) = (◡𝐹 “ {0, 𝑦})) |
120 | 119 | eleq1d 2823 |
. . . . . . 7
⊢ (𝐽 = {0, 𝑦} → ((◡𝐹 “ 𝐽) ∈ 𝐼 ↔ (◡𝐹 “ {0, 𝑦}) ∈ 𝐼)) |
121 | 118, 120 | imbi12d 344 |
. . . . . 6
⊢ (𝐽 = {0, 𝑦} → ((𝐽 ⊆ (0...𝑁) → (◡𝐹 “ 𝐽) ∈ 𝐼) ↔ ({0, 𝑦} ⊆ (0...𝑁) → (◡𝐹 “ {0, 𝑦}) ∈ 𝐼))) |
122 | 117, 121 | syl5ibrcom 247 |
. . . . 5
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) → (◡𝐹 “ 𝐽) ∈ 𝐼))) |
123 | 122 | rexlimdva 3152 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) → (◡𝐹 “ 𝐽) ∈ 𝐼))) |
124 | 123 | impcomd 411 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ((𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦}) → (◡𝐹 “ 𝐽) ∈ 𝐼)) |
125 | 3, 124 | sylbid 240 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) → (◡𝐹 “ 𝐽) ∈ 𝐼)) |
126 | 125 | 3impia 1116 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼) |