Proof of Theorem wlkl0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | clwlkwlk 29796 | . . . . . . . 8
⊢ (𝑤 ∈ (ClWalks‘𝐺) → 𝑤 ∈ (Walks‘𝐺)) | 
| 2 |  | wlkop 29647 | . . . . . . . 8
⊢ (𝑤 ∈ (Walks‘𝐺) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 3 | 1, 2 | syl 17 | . . . . . . 7
⊢ (𝑤 ∈ (ClWalks‘𝐺) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 4 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢
(1st ‘𝑤) ∈ V | 
| 5 |  | hasheq0 14403 | . . . . . . . . . . . . . . 15
⊢
((1st ‘𝑤) ∈ V →
((♯‘(1st ‘𝑤)) = 0 ↔ (1st ‘𝑤) = ∅)) | 
| 6 | 4, 5 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
((♯‘(1st ‘𝑤)) = 0 ↔ (1st ‘𝑤) = ∅) | 
| 7 | 6 | biimpi 216 | . . . . . . . . . . . . 13
⊢
((♯‘(1st ‘𝑤)) = 0 → (1st ‘𝑤) = ∅) | 
| 8 | 7 | adantr 480 | . . . . . . . . . . . 12
⊢
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → (1st ‘𝑤) = ∅) | 
| 9 | 8 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ (1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) → (1st ‘𝑤) = ∅) | 
| 10 | 8 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → (1st ‘𝑤) = ∅) | 
| 11 | 10 | breq1d 5152 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ↔
∅(ClWalks‘𝐺)(2nd ‘𝑤))) | 
| 12 |  | clwlknon2num.v | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑉 = (Vtx‘𝐺) | 
| 13 | 12 | 1vgrex 29020 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝑉 → 𝐺 ∈ V) | 
| 14 | 12 | 0clwlk 30150 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ V →
(∅(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd ‘𝑤):(0...0)⟶𝑉)) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑉 → (∅(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd
‘𝑤):(0...0)⟶𝑉)) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → (∅(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd
‘𝑤):(0...0)⟶𝑉)) | 
| 17 | 11, 16 | bitrd 279 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ↔ (2nd
‘𝑤):(0...0)⟶𝑉)) | 
| 18 |  | fz0sn 13668 | . . . . . . . . . . . . . . . . 17
⊢ (0...0) =
{0} | 
| 19 | 18 | feq2i 6727 | . . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑤):(0...0)⟶𝑉 ↔ (2nd ‘𝑤):{0}⟶𝑉) | 
| 20 |  | c0ex 11256 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V | 
| 21 | 20 | fsn2 7155 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑤):{0}⟶𝑉 ↔ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) | 
| 22 |  | simprr 772 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉}) | 
| 23 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((2nd ‘𝑤)‘0) = 𝑋) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → ((2nd
‘𝑤)‘0) = 𝑋) | 
| 25 | 24 | opeq2d 4879 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → 〈0,
((2nd ‘𝑤)‘0)〉 = 〈0, 𝑋〉) | 
| 26 | 25 | sneqd 4637 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → {〈0,
((2nd ‘𝑤)‘0)〉} = {〈0, 𝑋〉}) | 
| 27 | 22, 26 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ∧ (((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉})) → (2nd
‘𝑤) = {〈0, 𝑋〉}) | 
| 28 | 27 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((((2nd ‘𝑤)‘0) ∈ 𝑉 ∧ (2nd
‘𝑤) = {〈0,
((2nd ‘𝑤)‘0)〉}) → (2nd
‘𝑤) = {〈0, 𝑋〉})) | 
| 29 | 21, 28 | biimtrid 242 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((2nd ‘𝑤):{0}⟶𝑉 → (2nd ‘𝑤) = {〈0, 𝑋〉})) | 
| 30 | 19, 29 | biimtrid 242 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((2nd ‘𝑤):(0...0)⟶𝑉 → (2nd
‘𝑤) = {〈0, 𝑋〉})) | 
| 31 | 17, 30 | sylbid 240 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑉 ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) → (2nd
‘𝑤) = {〈0, 𝑋〉})) | 
| 32 | 31 | ex 412 | . . . . . . . . . . . . 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 4880 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ (1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉) | 
| 36 | 35 | 3exp 1119 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → ((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉))) | 
| 37 |  | eleq1 2828 | . . . . . . . . . . 11
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ (ClWalks‘𝐺))) | 
| 38 |  | df-br 5143 | . . . . . . . . . . 11
⊢
((1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) ↔ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈
(ClWalks‘𝐺)) | 
| 39 | 37, 38 | bitr4di 289 | . . . . . . . . . 10
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
(1st ‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤))) | 
| 40 |  | eqeq1 2740 | . . . . . . . . . . 11
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
(𝑤 = 〈∅,
{〈0, 𝑋〉}〉
↔ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅, {〈0, 𝑋〉}〉)) | 
| 41 | 40 | imbi2d 340 | . . . . . . . . . 10
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
((((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉) ↔
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉))) | 
| 42 | 39, 41 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑤 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉 →
((𝑤 ∈
(ClWalks‘𝐺) →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) ↔ ((1st
‘𝑤)(ClWalks‘𝐺)(2nd ‘𝑤) → (((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋) → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 = 〈∅,
{〈0, 𝑋〉}〉)))) | 
| 43 | 36, 42 | imbitrrid 246 | . . . . . . . 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 410 | . . . 4
⊢ (𝑋 ∈ 𝑉 → ((𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) → 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) | 
| 48 |  | eqidd 2737 | . . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ∅ = ∅) | 
| 49 | 20 | a1i 11 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 0 ∈ V) | 
| 50 |  | snidg 4659 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) | 
| 51 | 49, 50 | fsnd 6890 | . . . . . . 7
⊢ (𝑋 ∈ 𝑉 → {〈0, 𝑋〉}:{0}⟶{𝑋}) | 
| 52 | 12 | 0clwlkv 30151 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∅ = ∅ ∧ {〈0,
𝑋〉}:{0}⟶{𝑋}) →
∅(ClWalks‘𝐺){〈0, 𝑋〉}) | 
| 53 | 48, 51, 52 | mpd3an23 1464 | . . . . . 6
⊢ (𝑋 ∈ 𝑉 → ∅(ClWalks‘𝐺){〈0, 𝑋〉}) | 
| 54 |  | hash0 14407 | . . . . . . 7
⊢
(♯‘∅) = 0 | 
| 55 | 54 | a1i 11 | . . . . . 6
⊢ (𝑋 ∈ 𝑉 → (♯‘∅) =
0) | 
| 56 |  | fvsng 7201 | . . . . . . 7
⊢ ((0
∈ V ∧ 𝑋 ∈
𝑉) → ({〈0, 𝑋〉}‘0) = 𝑋) | 
| 57 | 20, 56 | mpan 690 | . . . . . 6
⊢ (𝑋 ∈ 𝑉 → ({〈0, 𝑋〉}‘0) = 𝑋) | 
| 58 | 53, 55, 57 | jca32 515 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → (∅(ClWalks‘𝐺){〈0, 𝑋〉} ∧ ((♯‘∅) = 0
∧ ({〈0, 𝑋〉}‘0) = 𝑋))) | 
| 59 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
〈∅, {〈0, 𝑋〉}〉 ∈ (ClWalks‘𝐺))) | 
| 60 |  | df-br 5143 | . . . . . . 7
⊢
(∅(ClWalks‘𝐺){〈0, 𝑋〉} ↔ 〈∅, {〈0,
𝑋〉}〉 ∈
(ClWalks‘𝐺)) | 
| 61 | 59, 60 | bitr4di 289 | . . . . . 6
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(𝑤 ∈
(ClWalks‘𝐺) ↔
∅(ClWalks‘𝐺){〈0, 𝑋〉})) | 
| 62 |  | 0ex 5306 | . . . . . . . . 9
⊢ ∅
∈ V | 
| 63 |  | snex 5435 | . . . . . . . . 9
⊢ {〈0,
𝑋〉} ∈
V | 
| 64 | 62, 63 | op1std 8025 | . . . . . . . 8
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(1st ‘𝑤) =
∅) | 
| 65 | 64 | fveqeq2d 6913 | . . . . . . 7
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
((♯‘(1st ‘𝑤)) = 0 ↔ (♯‘∅) =
0)) | 
| 66 | 62, 63 | op2ndd 8026 | . . . . . . . . 9
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(2nd ‘𝑤) =
{〈0, 𝑋〉}) | 
| 67 | 66 | fveq1d 6907 | . . . . . . . 8
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
((2nd ‘𝑤)‘0) = ({〈0, 𝑋〉}‘0)) | 
| 68 | 67 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(((2nd ‘𝑤)‘0) = 𝑋 ↔ ({〈0, 𝑋〉}‘0) = 𝑋)) | 
| 69 | 65, 68 | anbi12d 632 | . . . . . 6
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
(((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋) ↔ ((♯‘∅) = 0 ∧
({〈0, 𝑋〉}‘0) = 𝑋))) | 
| 70 | 61, 69 | anbi12d 632 | . . . . 5
⊢ (𝑤 = 〈∅, {〈0,
𝑋〉}〉 →
((𝑤 ∈
(ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) ↔ (∅(ClWalks‘𝐺){〈0, 𝑋〉} ∧ ((♯‘∅) = 0
∧ ({〈0, 𝑋〉}‘0) = 𝑋)))) | 
| 71 | 58, 70 | syl5ibrcom 247 | . . . 4
⊢ (𝑋 ∈ 𝑉 → (𝑤 = 〈∅, {〈0, 𝑋〉}〉 → (𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)))) | 
| 72 | 47, 71 | impbid 212 | . . 3
⊢ (𝑋 ∈ 𝑉 → ((𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ↔ 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) | 
| 73 | 72 | alrimiv 1926 | . 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑤((𝑤 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)) ↔ 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) | 
| 74 |  | rabeqsn 4666 | . 2
⊢ ({𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} = {〈∅, {〈0, 𝑋〉}〉} ↔
∀𝑤((𝑤 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)) ↔ 𝑤 = 〈∅, {〈0, 𝑋〉}〉)) | 
| 75 | 73, 74 | sylibr 234 | 1
⊢ (𝑋 ∈ 𝑉 → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 0 ∧
((2nd ‘𝑤)‘0) = 𝑋)} = {〈∅, {〈0, 𝑋〉}〉}) |