Proof of Theorem wlkl0
Step | Hyp | Ref
| Expression |
1 | | clwlkwlk 28143 |
. . . . . . . 8
⊢ (𝑤 ∈ (ClWalks‘𝐺) → 𝑤 ∈ (Walks‘𝐺)) |
2 | | wlkop 27995 |
. . . . . . . 8
⊢ (𝑤 ∈ (Walks‘𝐺) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝑤 ∈ (ClWalks‘𝐺) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
4 | | fvex 6787 |
. . . . . . . . . . . . . . 15
⊢
(1st ‘𝑤) ∈ V |
5 | | hasheq0 14078 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑤) ∈ V →
((♯‘(1st ‘𝑤)) = 0 ↔ (1st ‘𝑤) = ∅)) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((♯‘(1st ‘𝑤)) = 0 ↔ (1st ‘𝑤) = ∅) |
7 | 6 | biimpi 215 |
. . . . . . . . . . . . 13
⊢
((♯‘(1st ‘𝑤)) = 0 → (1st ‘𝑤) = ∅) |
8 | 7 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → (1st ‘𝑤) = ∅) |
9 | 8 | 3ad2ant3 1134 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ (1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) → (1st ‘𝑤) = ∅) |
10 | 8 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → (1st ‘𝑤) = ∅) |
11 | 10 | breq1d 5084 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ↔
∅(ClWalks‘𝐺)(2nd ‘𝑤))) |
12 | | clwlknon2num.v |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑉 = (Vtx‘𝐺) |
13 | 12 | 1vgrex 27372 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝑉 → 𝐺 ∈ V) |
14 | 12 | 0clwlk 28494 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ V →
(∅(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd ‘𝑤):(0...0)⟶𝑉)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑉 → (∅(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd
‘𝑤):(0...0)⟶𝑉)) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → (∅(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd
‘𝑤):(0...0)⟶𝑉)) |
17 | 11, 16 | bitrd 278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd
‘𝑤):(0...0)⟶𝑉)) |
18 | | fz0sn 13356 |
. . . . . . . . . . . . . . . . 17
⊢ (0...0) =
{0} |
19 | 18 | feq2i 6592 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑤):(0...0)⟶𝑉 ↔ (2nd ‘𝑤):{0}⟶𝑉) |
20 | | c0ex 10969 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
21 | 20 | fsn2 7008 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑤):{0}⟶𝑉 ↔ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) |
22 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉}) |
23 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((2nd ‘𝑤)‘0) = 𝑋) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → ((2nd
‘𝑤)‘0) = 𝑋) |
25 | 24 | opeq2d 4811 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → 〈0,
((2nd ‘𝑤)‘0)〉 = 〈0, 𝑋〉) |
26 | 25 | sneqd 4573 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → {〈0,
((2nd ‘𝑤)‘0)〉} = {〈0, 𝑋〉}) |
27 | 22, 26 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → (2nd
‘𝑤) = {〈0, 𝑋〉}) |
28 | 27 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉}) → (2nd
‘𝑤) = {〈0, 𝑋〉})) |
29 | 21, 28 | syl5bi 241 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((2nd ‘𝑤):{0}⟶𝑉 → (2nd ‘𝑤) = {〈0, 𝑋〉})) |
30 | 19, 29 | syl5bi 241 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((2nd ‘𝑤):(0...0)⟶𝑉 → (2nd
‘𝑤) = {〈0, 𝑋〉})) |
31 | 17, 30 | sylbid 239 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) → (2nd
‘𝑤) = {〈0, 𝑋〉})) |
32 | 31 | ex 413 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑉 → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) → (2nd
‘𝑤) = {〈0, 𝑋〉}))) |
33 | 32 | com23 86 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑉 → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → (2nd ‘𝑤) = {〈0, 𝑋〉}))) |
34 | 33 | 3imp 1110 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ (1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) → (2nd ‘𝑤) = {〈0, 𝑋〉}) |
35 | 9, 34 | opeq12d 4812 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ (1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉) |
36 | 35 | 3exp 1118 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉))) |
37 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ (ClWalks‘𝐺))) |
38 | | df-br 5075 |
. . . . . . . . . . 11
⊢
((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ↔ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈
(ClWalks‘𝐺)) |
39 | 37, 38 | bitr4di 289 |
. . . . . . . . . 10
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
(1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤))) |
40 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 = 〈∅,
{〈0, 𝑋〉}〉
↔ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅, {〈0, 𝑋〉}〉)) |
41 | 40 | imbi2d 341 |
. . . . . . . . . 10
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
((((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉) ↔
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉))) |
42 | 39, 41 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
((𝑤 ∈
(ClWalks‘𝐺) →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) ↔ ((1st
‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉)))) |
43 | 36, 42 | syl5ibr 245 |
. . . . . . . 8
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑋 ∈ 𝑉 → (𝑤 ∈ (ClWalks‘𝐺) → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉)))) |
44 | 43 | com23 86 |
. . . . . . 7
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 ∈
(ClWalks‘𝐺) →
(𝑋 ∈ 𝑉 → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉)))) |
45 | 3, 44 | mpcom 38 |
. . . . . 6
⊢ (𝑤 ∈ (ClWalks‘𝐺) → (𝑋 ∈ 𝑉 → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉))) |
46 | 45 | com12 32 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑤 ∈ (ClWalks‘𝐺) → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉))) |
47 | 46 | impd 411 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → ((𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) |
48 | | eqidd 2739 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ∅ = ∅) |
49 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 0 ∈ V) |
50 | | snidg 4595 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
51 | 49, 50 | fsnd 6759 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → {〈0, 𝑋〉}:{0}⟶{𝑋}) |
52 | 12 | 0clwlkv 28495 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∅ = ∅ ∧ {〈0,
𝑋〉}:{0}⟶{𝑋}) →
∅(ClWalks‘𝐺){〈0, 𝑋〉}) |
53 | 48, 51, 52 | mpd3an23 1462 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ∅(ClWalks‘𝐺){〈0, 𝑋〉}) |
54 | | hash0 14082 |
. . . . . . 7
⊢
(♯‘∅) = 0 |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (♯‘∅) =
0) |
56 | | fvsng 7052 |
. . . . . . 7
⊢ ((0
∈ V ∧ 𝑋 ∈
𝑉) → ({〈0, 𝑋〉}‘0) = 𝑋) |
57 | 20, 56 | mpan 687 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ({〈0, 𝑋〉}‘0) = 𝑋) |
58 | 53, 55, 57 | jca32 516 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (∅(ClWalks‘𝐺){〈0, 𝑋〉} ∧ ((♯‘∅) = 0
∧ ({〈0, 𝑋〉}‘0) = 𝑋))) |
59 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
〈∅, {〈0, 𝑋〉}〉 ∈ (ClWalks‘𝐺))) |
60 | | df-br 5075 |
. . . . . . 7
⊢
(∅(ClWalks‘𝐺){〈0, 𝑋〉} ↔ 〈∅, {〈0,
𝑋〉}〉 ∈
(ClWalks‘𝐺)) |
61 | 59, 60 | bitr4di 289 |
. . . . . 6
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
∅(ClWalks‘𝐺){〈0, 𝑋〉})) |
62 | | 0ex 5231 |
. . . . . . . . 9
⊢ ∅
∈ V |
63 | | snex 5354 |
. . . . . . . . 9
⊢ {〈0,
𝑋〉} ∈
V |
64 | 62, 63 | op1std 7841 |
. . . . . . . 8
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(1st ‘𝑤) =
∅) |
65 | 64 | fveqeq2d 6782 |
. . . . . . 7
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
((♯‘(1st ‘𝑤)) = 0 ↔ (♯‘∅) =
0)) |
66 | 62, 63 | op2ndd 7842 |
. . . . . . . . 9
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(2nd ‘𝑤) =
{〈0, 𝑋〉}) |
67 | 66 | fveq1d 6776 |
. . . . . . . 8
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
((2nd ‘𝑤)‘0) = ({〈0, 𝑋〉}‘0)) |
68 | 67 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(((2nd ‘𝑤)‘0) = 𝑋 ↔ ({〈0, 𝑋〉}‘0) = 𝑋)) |
69 | 65, 68 | anbi12d 631 |
. . . . . 6
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) ↔ ((♯‘∅) = 0 ∧
({〈0, 𝑋〉}‘0) = 𝑋))) |
70 | 61, 69 | anbi12d 631 |
. . . . 5
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
((𝑤 ∈
(ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) ↔ (∅(ClWalks‘𝐺){〈0, 𝑋〉} ∧ ((♯‘∅) = 0
∧ ({〈0, 𝑋〉}‘0) = 𝑋)))) |
71 | 58, 70 | syl5ibrcom 246 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (𝑤 = 〈∅, {〈0, 𝑋〉}〉 → (𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)))) |
72 | 47, 71 | impbid 211 |
. . 3
⊢ (𝑋 ∈ 𝑉 → ((𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ↔ 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) |
73 | 72 | alrimiv 1930 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑤((𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ↔ 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) |
74 | | rabeqsn 4602 |
. 2
⊢ ({𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} = {〈∅, {〈0, 𝑋〉}〉} ↔
∀𝑤((𝑤 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) ↔ 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) |
75 | 73, 74 | sylibr 233 |
1
⊢ (𝑋 ∈ 𝑉 → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)} = {〈∅, {〈0, 𝑋〉}〉}) |