Step | Hyp | Ref
| Expression |
1 | | f1oi 6886 |
. . . . 5
⊢ ( I
↾ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1-onto→{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} |
2 | | f1of1 6847 |
. . . . 5
⊢ (( I
↾ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1-onto→{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} → ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1→{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) |
3 | 1, 2 | mp1i 13 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ( I ↾ {𝑒
∈ 𝒫 (0...𝑁)
∣ ∃𝑥 ∈
(1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1→{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) |
4 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) ∧ 𝑥 ∈ (1...𝑁)) ∧ 𝑘 = {0, 𝑥}) → 𝑘 ∈ 𝒫 (0...𝑁)) |
5 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = {0, 𝑥} → (♯‘𝑘) = (♯‘{0, 𝑥})) |
6 | | 0red 11261 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝑁) → 0 ∈ ℝ) |
7 | | elfznn 13589 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
8 | 7 | nngt0d 12312 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝑁) → 0 < 𝑥) |
9 | 6, 8 | ltned 11394 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑁) → 0 ≠ 𝑥) |
10 | | c0ex 11252 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
11 | | vex 3481 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
12 | 10, 11 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
V ∧ 𝑥 ∈
V) |
13 | | hashprg 14430 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ V ∧ 𝑥 ∈ V)
→ (0 ≠ 𝑥 ↔
(♯‘{0, 𝑥}) =
2)) |
14 | 12, 13 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑁) → (0 ≠ 𝑥 ↔ (♯‘{0, 𝑥}) = 2)) |
15 | 9, 14 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝑁) → (♯‘{0, 𝑥}) = 2) |
16 | 15 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) ∧ 𝑥 ∈ (1...𝑁)) → (♯‘{0, 𝑥}) = 2) |
17 | 5, 16 | sylan9eqr 2796 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) ∧ 𝑥 ∈ (1...𝑁)) ∧ 𝑘 = {0, 𝑥}) → (♯‘𝑘) = 2) |
18 | 4, 17 | jca 511 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) ∧ 𝑥 ∈ (1...𝑁)) ∧ 𝑘 = {0, 𝑥}) → (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2)) |
19 | 18 | ex 412 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) ∧ 𝑥 ∈ (1...𝑁)) → (𝑘 = {0, 𝑥} → (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2))) |
20 | 19 | rexlimdva 3152 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) →
(∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥} → (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2))) |
21 | 20 | expimpd 453 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑘 ∈ 𝒫
(0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥}) → (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2))) |
22 | | eqeq1 2738 |
. . . . . . . 8
⊢ (𝑒 = 𝑘 → (𝑒 = {0, 𝑥} ↔ 𝑘 = {0, 𝑥})) |
23 | 22 | rexbidv 3176 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → (∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥} ↔ ∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥})) |
24 | 23 | elrab 3694 |
. . . . . 6
⊢ (𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} ↔ (𝑘 ∈ 𝒫 (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥})) |
25 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → ((♯‘𝑒) = 2 ↔ (♯‘𝑘) = 2)) |
26 | 25 | elrab 3694 |
. . . . . 6
⊢ (𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2} ↔ (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2)) |
27 | 21, 24, 26 | 3imtr4g 296 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} → 𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2})) |
28 | 27 | ssrdv 4000 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} ⊆ {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2}) |
29 | | f1ss 6809 |
. . . 4
⊢ ((( I
↾ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1→{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} ∧ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} ⊆ {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2}) → ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1→{𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2}) |
30 | 3, 28, 29 | syl2anc 584 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ( I ↾ {𝑒
∈ 𝒫 (0...𝑁)
∣ ∃𝑥 ∈
(1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1→{𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2}) |
31 | | stgriedg 47857 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) |
32 | 31 | dmeqd 5918 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ dom (iEdg‘(StarGr‘𝑁)) = dom ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) |
33 | | dmresi 6071 |
. . . . 5
⊢ dom ( I
↾ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} |
34 | 32, 33 | eqtrdi 2790 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ dom (iEdg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) |
35 | | stgrvtx 47856 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) |
36 | 35 | pweqd 4621 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝒫 (Vtx‘(StarGr‘𝑁)) = 𝒫 (0...𝑁)) |
37 | 36 | rabeqdv 3448 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ {𝑒 ∈ 𝒫
(Vtx‘(StarGr‘𝑁)) ∣ (♯‘𝑒) = 2} = {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2}) |
38 | 31, 34, 37 | f1eq123d 6840 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((iEdg‘(StarGr‘𝑁)):dom (iEdg‘(StarGr‘𝑁))–1-1→{𝑒 ∈ 𝒫
(Vtx‘(StarGr‘𝑁)) ∣ (♯‘𝑒) = 2} ↔ ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}):{𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}–1-1→{𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2})) |
39 | 30, 38 | mpbird 257 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (iEdg‘(StarGr‘𝑁)):dom (iEdg‘(StarGr‘𝑁))–1-1→{𝑒 ∈ 𝒫
(Vtx‘(StarGr‘𝑁)) ∣ (♯‘𝑒) = 2}) |
40 | | fvex 6919 |
. . 3
⊢
(StarGr‘𝑁)
∈ V |
41 | | eqid 2734 |
. . . 4
⊢
(Vtx‘(StarGr‘𝑁)) = (Vtx‘(StarGr‘𝑁)) |
42 | | eqid 2734 |
. . . 4
⊢
(iEdg‘(StarGr‘𝑁)) = (iEdg‘(StarGr‘𝑁)) |
43 | 41, 42 | isusgrs 29187 |
. . 3
⊢
((StarGr‘𝑁)
∈ V → ((StarGr‘𝑁) ∈ USGraph ↔
(iEdg‘(StarGr‘𝑁)):dom (iEdg‘(StarGr‘𝑁))–1-1→{𝑒 ∈ 𝒫
(Vtx‘(StarGr‘𝑁)) ∣ (♯‘𝑒) = 2})) |
44 | 40, 43 | mp1i 13 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((StarGr‘𝑁)
∈ USGraph ↔ (iEdg‘(StarGr‘𝑁)):dom (iEdg‘(StarGr‘𝑁))–1-1→{𝑒 ∈ 𝒫
(Vtx‘(StarGr‘𝑁)) ∣ (♯‘𝑒) = 2})) |
45 | 39, 44 | mpbird 257 |
1
⊢ (𝑁 ∈ ℕ0
→ (StarGr‘𝑁)
∈ USGraph) |