| 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 11264 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝑁) → 0 ∈ ℝ) |
| 7 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
| 8 | 7 | nngt0d 12315 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝑁) → 0 < 𝑥) |
| 9 | 6, 8 | ltned 11397 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑁) → 0 ≠ 𝑥) |
| 10 | | c0ex 11255 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
| 11 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 12 | 10, 11 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
V ∧ 𝑥 ∈
V) |
| 13 | | hashprg 14434 |
. . . . . . . . . . . . . 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 2799 |
. . . . . . . . . 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 3155 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ 𝒫
(0...𝑁)) →
(∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥} → (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2))) |
| 21 | 20 | expimpd 453 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑘 ∈ 𝒫
(0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥}) → (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2))) |
| 22 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑒 = 𝑘 → (𝑒 = {0, 𝑥} ↔ 𝑘 = {0, 𝑥})) |
| 23 | 22 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → (∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥} ↔ ∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥})) |
| 24 | 23 | elrab 3692 |
. . . . . 6
⊢ (𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} ↔ (𝑘 ∈ 𝒫 (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝑘 = {0, 𝑥})) |
| 25 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑒 = 𝑘 → ((♯‘𝑒) = 2 ↔ (♯‘𝑘) = 2)) |
| 26 | 25 | elrab 3692 |
. . . . . 6
⊢ (𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2} ↔ (𝑘 ∈ 𝒫 (0...𝑁) ∧ (♯‘𝑘) = 2)) |
| 27 | 21, 24, 26 | 3imtr4g 296 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} → 𝑘 ∈ {𝑒 ∈ 𝒫 (0...𝑁) ∣ (♯‘𝑒) = 2})) |
| 28 | 27 | ssrdv 3989 |
. . . 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 47922 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) |
| 32 | 31 | dmeqd 5916 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ dom (iEdg‘(StarGr‘𝑁)) = dom ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) |
| 33 | | dmresi 6070 |
. . . . 5
⊢ dom ( I
↾ {𝑒 ∈ 𝒫
(0...𝑁) ∣
∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}} |
| 34 | 32, 33 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ dom (iEdg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) |
| 35 | | stgrvtx 47921 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) |
| 36 | 35 | pweqd 4617 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝒫 (Vtx‘(StarGr‘𝑁)) = 𝒫 (0...𝑁)) |
| 37 | 36 | rabeqdv 3452 |
. . . 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 2737 |
. . . 4
⊢
(Vtx‘(StarGr‘𝑁)) = (Vtx‘(StarGr‘𝑁)) |
| 42 | | eqid 2737 |
. . . 4
⊢
(iEdg‘(StarGr‘𝑁)) = (iEdg‘(StarGr‘𝑁)) |
| 43 | 41, 42 | isusgrs 29173 |
. . 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) |