| Step | Hyp | Ref
| Expression |
| 1 | | isubgr3stgr.n |
. . . 4
⊢ 𝑁 ∈
ℕ0 |
| 2 | | stgredgel 47924 |
. . . 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 11255 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 5 | 4 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V) |
| 6 | | prssg 4819 |
. . . . . . . . . . . 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 47921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) |
| 14 | 1, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Vtx‘(StarGr‘𝑁)) = (0...𝑁) |
| 15 | 10, 12, 14 | 3eqtri 2769 |
. . . . . . . . . . . . . . . . . . 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 1095 |
. . . . . . . . . . . . 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 6992 |
. . . . . . . . 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 47816 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋)) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋)) |
| 32 | | isubgr3stgr.c |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) |
| 33 | 31, 32 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . 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 7298 |
. . . . . . . . . . . . 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 2852 |
. . . . . . . . . . . . . . 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 13663 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑁) ⊆
(0...𝑁) |
| 49 | 48 | sseli 3979 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ (0...𝑁)) |
| 50 | 49, 15 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ 𝑊) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑦 ∈ 𝑊) |
| 52 | 47, 51 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (◡𝐹‘𝑦) ∈ 𝐶) |
| 53 | 43, 52 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑋 ∈ 𝐶 ∧ (◡𝐹‘𝑦) ∈ 𝐶)) |
| 54 | 32 | eleq2i 2833 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹‘𝑦) ∈ 𝐶 ↔ (◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋)) |
| 55 | | usgrupgr 29202 |
. . . . . . . . . . . . . . . . . . . . . 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 47818 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉 |
| 59 | 32, 58 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐶 ⊆ 𝑉 |
| 60 | 59, 52 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (◡𝐹‘𝑦) ∈ 𝑉) |
| 61 | | df-3an 1089 |
. . . . . . . . . . . . . . . . . . . 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 47821 |
. . . . . . . . . . . . . . . . . 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 2749 |
. . . . . . . . . . . . . . . . . . . 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 13664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
| 74 | 1, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
(0...𝑁) |
| 75 | 74, 15 | eleqtrri 2840 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
𝑊 |
| 76 | 50, 75 | jctir 520 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (1...𝑁) → (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) |
| 77 | | f1veqaeq 7277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡𝐹:𝑊–1-1→𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((◡𝐹‘𝑦) = (◡𝐹‘0) → 𝑦 = 0)) |
| 78 | 72, 76, 77 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((◡𝐹‘𝑦) = (◡𝐹‘0) → 𝑦 = 0)) |
| 79 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ) |
| 80 | | nnne0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
| 81 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . . . . . . . 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 4732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {(◡𝐹‘𝑦), 𝑋} = {𝑋, (◡𝐹‘𝑦)} |
| 90 | 89 | eleq1i 2832 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({(◡𝐹‘𝑦), 𝑋} ∈ 𝐸 ↔ {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸) |
| 91 | 90 | biimpi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ ({(◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸) |
| 92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ({(◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
| 93 | 88, 92 | jaod 860 |
. . . . . . . . . . . . . . . 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 4821 |
. . . . . . . . . . . . . . 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 4733 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹‘0) = 𝑋 → {(◡𝐹‘0), (◡𝐹‘𝑦)} = {𝑋, (◡𝐹‘𝑦)}) |
| 101 | 100 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹‘0) = 𝑋 → ({(◡𝐹‘0), (◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (◡𝐹‘𝑦)} ∈ 𝐸)) |
| 102 | 100 | sseq1d 4015 |
. . . . . . . . . . . . . 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 29203 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UHGraph) |
| 109 | 108 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝐺 ∈ UHGraph) |
| 110 | 59 | a1i 11 |
. . . . . . . . . 10
⊢ ({0,
𝑦} ⊆ (0...𝑁) → 𝐶 ⊆ 𝑉) |
| 111 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶) |
| 112 | | isubgr3stgr.i |
. . . . . . . . . . 11
⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) |
| 113 | 29, 64, 111, 112 | isubgredg 47852 |
. . . . . . . . . 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 2841 |
. . . . . . 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 4009 |
. . . . . . 7
⊢ (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) ↔ {0, 𝑦} ⊆ (0...𝑁))) |
| 119 | | imaeq2 6074 |
. . . . . . . 8
⊢ (𝐽 = {0, 𝑦} → (◡𝐹 “ 𝐽) = (◡𝐹 “ {0, 𝑦})) |
| 120 | 119 | eleq1d 2826 |
. . . . . . 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 3155 |
. . . 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 1118 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼) |