Step | Hyp | Ref
| Expression |
1 | | f1oi 6086 |
. . . . 5
⊢ ( I
↾ 𝐹):𝐹–1-1-onto→𝐹 |
2 | | f1of 6050 |
. . . . 5
⊢ (( I
↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹⟶𝐹) |
3 | 1, 2 | mp1i 13 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ( I ↾ 𝐹):𝐹⟶𝐹) |
4 | | dmresi 5376 |
. . . . . 6
⊢ dom ( I
↾ 𝐹) = 𝐹 |
5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → dom ( I ↾ 𝐹) = 𝐹) |
6 | 5 | feq2d 5944 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐹 ↔ ( I ↾ 𝐹):𝐹⟶𝐹)) |
7 | 3, 6 | mpbird 246 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐹) |
8 | | upgrres1.f |
. . . . 5
⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} |
9 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝐸) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → 𝑒 ∈ 𝐸) |
11 | | upgrres1.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (Edg‘𝐺) |
12 | 11 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ (Edg‘𝐺)) |
13 | | edgupgr 25808 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UPGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝑒 ≠ ∅ ∧ (#‘𝑒) ≤ 2)) |
14 | | elpwi 4117 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ 𝒫
(Vtx‘𝐺) → 𝑒 ⊆ (Vtx‘𝐺)) |
15 | | upgrres1.v |
. . . . . . . . . . . . . . 15
⊢ 𝑉 = (Vtx‘𝐺) |
16 | 14, 15 | syl6sseqr 3615 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ 𝒫
(Vtx‘𝐺) → 𝑒 ⊆ 𝑉) |
17 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ 𝒫
(Vtx‘𝐺) ∧ 𝑒 ≠ ∅ ∧
(#‘𝑒) ≤ 2) →
𝑒 ⊆ 𝑉) |
18 | 13, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → 𝑒 ⊆ 𝑉) |
19 | 12, 18 | sylan2b 491 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸) → 𝑒 ⊆ 𝑉) |
20 | 19 | ad4ant13 1284 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → 𝑒 ⊆ 𝑉) |
21 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → 𝑁 ∉ 𝑒) |
22 | | elpwdifsn 40312 |
. . . . . . . . . 10
⊢ ((𝑒 ∈ 𝐸 ∧ 𝑒 ⊆ 𝑉 ∧ 𝑁 ∉ 𝑒) → 𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁})) |
23 | 10, 20, 21, 22 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → 𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁})) |
24 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝐺 ∈ UPGraph ) |
25 | 12 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 → 𝑒 ∈ (Edg‘𝐺)) |
26 | 13 | simp2d 1067 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → 𝑒 ≠ ∅) |
27 | 24, 25, 26 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → 𝑒 ≠ ∅) |
28 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → 𝑒 ≠ ∅) |
29 | | nelsn 4159 |
. . . . . . . . . 10
⊢ (𝑒 ≠ ∅ → ¬ 𝑒 ∈
{∅}) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → ¬ 𝑒 ∈ {∅}) |
31 | 23, 30 | eldifd 3551 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) ∧ 𝑁 ∉ 𝑒) → 𝑒 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅})) |
32 | 31 | ex 449 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → (𝑁 ∉ 𝑒 → 𝑒 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}))) |
33 | 32 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ∀𝑒 ∈ 𝐸 (𝑁 ∉ 𝑒 → 𝑒 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}))) |
34 | | rabss 3642 |
. . . . . 6
⊢ ({𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⊆ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ↔ ∀𝑒 ∈ 𝐸 (𝑁 ∉ 𝑒 → 𝑒 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}))) |
35 | 33, 34 | sylibr 223 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⊆ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅})) |
36 | 8, 35 | syl5eqss 3612 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝐹 ⊆ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅})) |
37 | | elrabi 3328 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} → 𝑝 ∈ 𝐸) |
38 | | edgaval 25794 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ UPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
39 | 11, 38 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UPGraph → 𝐸 = ran (iEdg‘𝐺)) |
40 | 39 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UPGraph → (𝑝 ∈ 𝐸 ↔ 𝑝 ∈ ran (iEdg‘𝐺))) |
41 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
42 | 15, 41 | upgrf 25753 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
43 | | frn 5966 |
. . . . . . . . . . . 12
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UPGraph → ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
45 | 44 | sseld 3567 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UPGraph → (𝑝 ∈ ran (iEdg‘𝐺) → 𝑝 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
46 | 40, 45 | sylbid 229 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph → (𝑝 ∈ 𝐸 → 𝑝 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
47 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑝 → (#‘𝑥) = (#‘𝑝)) |
48 | 47 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑝 → ((#‘𝑥) ≤ 2 ↔ (#‘𝑝) ≤ 2)) |
49 | 48 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑝 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔ (𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝑝) ≤
2)) |
50 | 49 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑝 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → (#‘𝑝) ≤ 2) |
51 | 46, 50 | syl6 34 |
. . . . . . . 8
⊢ (𝐺 ∈ UPGraph → (𝑝 ∈ 𝐸 → (#‘𝑝) ≤ 2)) |
52 | 51 | adantr 480 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝑝 ∈ 𝐸 → (#‘𝑝) ≤ 2)) |
53 | 37, 52 | syl5com 31 |
. . . . . 6
⊢ (𝑝 ∈ {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (#‘𝑝) ≤ 2)) |
54 | 53, 8 | eleq2s 2706 |
. . . . 5
⊢ (𝑝 ∈ 𝐹 → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (#‘𝑝) ≤ 2)) |
55 | 54 | impcom 445 |
. . . 4
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑝 ∈ 𝐹) → (#‘𝑝) ≤ 2) |
56 | 36, 55 | ssrabdv 3644 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝐹 ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (#‘𝑝) ≤ 2}) |
57 | 7, 56 | fssd 5970 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶{𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (#‘𝑝) ≤ 2}) |
58 | | upgrres1.s |
. . . 4
⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 |
59 | | opex 4859 |
. . . 4
⊢
〈(𝑉 ∖
{𝑁}), ( I ↾ 𝐹)〉 ∈
V |
60 | 58, 59 | eqeltri 2684 |
. . 3
⊢ 𝑆 ∈ V |
61 | 15, 11, 8, 58 | upgrres1lem2 40530 |
. . . . 5
⊢
(Vtx‘𝑆) =
(𝑉 ∖ {𝑁}) |
62 | 61 | eqcomi 2619 |
. . . 4
⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆) |
63 | 15, 11, 8, 58 | upgrres1lem3 40531 |
. . . . 5
⊢
(iEdg‘𝑆) = ( I
↾ 𝐹) |
64 | 63 | eqcomi 2619 |
. . . 4
⊢ ( I
↾ 𝐹) =
(iEdg‘𝑆) |
65 | 62, 64 | isupgr 25751 |
. . 3
⊢ (𝑆 ∈ V → (𝑆 ∈ UPGraph ↔ ( I
↾ 𝐹):dom ( I ↾
𝐹)⟶{𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (#‘𝑝) ≤ 2})) |
66 | 60, 65 | mp1i 13 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝑆 ∈ UPGraph ↔ ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶{𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (#‘𝑝) ≤ 2})) |
67 | 57, 66 | mpbird 246 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph ) |