Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | efgval.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
3 | | efgval2.m |
. . 3
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
4 | | efgval2.t |
. . 3
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
5 | 1, 2, 3, 4 | efgval2 17960 |
. 2
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} |
6 | | efgrelexlem.1 |
. . . . . . . 8
⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)} |
7 | 6 | relopabi 5167 |
. . . . . . 7
⊢ Rel 𝐿 |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (⊤
→ Rel 𝐿) |
9 | | simpr 476 |
. . . . . . 7
⊢
((⊤ ∧ 𝑓𝐿𝑔) → 𝑓𝐿𝑔) |
10 | | eqcom 2617 |
. . . . . . . . . 10
⊢ ((𝑎‘0) = (𝑏‘0) ↔ (𝑏‘0) = (𝑎‘0)) |
11 | 10 | 2rexbii 3024 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑏‘0) = (𝑎‘0)) |
12 | | rexcom 3080 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑏‘0) = (𝑎‘0) ↔ ∃𝑏 ∈ (◡𝑆 “ {𝑔})∃𝑎 ∈ (◡𝑆 “ {𝑓})(𝑏‘0) = (𝑎‘0)) |
13 | 11, 12 | bitri 263 |
. . . . . . . 8
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑏 ∈ (◡𝑆 “ {𝑔})∃𝑎 ∈ (◡𝑆 “ {𝑓})(𝑏‘0) = (𝑎‘0)) |
14 | | efgred.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
15 | | efgred.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
16 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 17985 |
. . . . . . . 8
⊢ (𝑓𝐿𝑔 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0)) |
17 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 17985 |
. . . . . . . 8
⊢ (𝑔𝐿𝑓 ↔ ∃𝑏 ∈ (◡𝑆 “ {𝑔})∃𝑎 ∈ (◡𝑆 “ {𝑓})(𝑏‘0) = (𝑎‘0)) |
18 | 13, 16, 17 | 3bitr4i 291 |
. . . . . . 7
⊢ (𝑓𝐿𝑔 ↔ 𝑔𝐿𝑓) |
19 | 9, 18 | sylib 207 |
. . . . . 6
⊢
((⊤ ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓) |
20 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 17985 |
. . . . . . . . 9
⊢ (𝑔𝐿ℎ ↔ ∃𝑟 ∈ (◡𝑆 “ {𝑔})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) |
21 | | reeanv 3086 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑟 ∈ (◡𝑆 “ {𝑔})(∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) ↔ (∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑟 ∈ (◡𝑆 “ {𝑔})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0))) |
22 | 1, 2, 3, 4, 14, 15 | efgsfo 17975 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑆:dom 𝑆–onto→𝑊 |
23 | | fofn 6030 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆:dom 𝑆–onto→𝑊 → 𝑆 Fn dom 𝑆) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑆 Fn dom 𝑆 |
25 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 Fn dom 𝑆 → (𝑟 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑔))) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑔)) |
27 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 Fn dom 𝑆 → (𝑏 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑔))) |
28 | 24, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑔)) |
29 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆‘𝑟) = 𝑔 ∧ (𝑆‘𝑏) = 𝑔) → (𝑆‘𝑟) = (𝑆‘𝑏)) |
30 | 1, 2, 3, 4, 14, 15 | efgred 17984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = (𝑆‘𝑏)) → (𝑟‘0) = (𝑏‘0)) |
31 | 30 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = (𝑆‘𝑏)) → (𝑏‘0) = (𝑟‘0)) |
32 | 31 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ (𝑆‘𝑟) = (𝑆‘𝑏)) → (𝑏‘0) = (𝑟‘0)) |
33 | 29, 32 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ ((𝑆‘𝑟) = 𝑔 ∧ (𝑆‘𝑏) = 𝑔)) → (𝑏‘0) = (𝑟‘0)) |
34 | 33 | an4s 865 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑔) ∧ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑔)) → (𝑏‘0) = (𝑟‘0)) |
35 | 26, 28, 34 | syl2anb 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → (𝑏‘0) = (𝑟‘0)) |
36 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟‘0) = (𝑠‘0) → ((𝑏‘0) = (𝑟‘0) ↔ (𝑏‘0) = (𝑠‘0))) |
37 | 35, 36 | syl5ibcom 234 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → ((𝑟‘0) = (𝑠‘0) → (𝑏‘0) = (𝑠‘0))) |
38 | 37 | reximdv 2999 |
. . . . . . . . . . . . . . 15
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑏‘0) = (𝑠‘0))) |
39 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎‘0) = (𝑏‘0) → ((𝑎‘0) = (𝑠‘0) ↔ (𝑏‘0) = (𝑠‘0))) |
40 | 39 | rexbidv 3034 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘0) = (𝑏‘0) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0) ↔ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑏‘0) = (𝑠‘0))) |
41 | 40 | imbi2d 329 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘0) = (𝑏‘0) → ((∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) ↔ (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑏‘0) = (𝑠‘0)))) |
42 | 38, 41 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → ((𝑎‘0) = (𝑏‘0) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)))) |
43 | 42 | rexlimdva 3013 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (◡𝑆 “ {𝑔}) → (∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)))) |
44 | 43 | impd 446 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ (◡𝑆 “ {𝑔}) → ((∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0))) |
45 | 44 | rexlimiv 3009 |
. . . . . . . . . . 11
⊢
(∃𝑟 ∈
(◡𝑆 “ {𝑔})(∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) |
46 | 45 | reximi 2994 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑟 ∈ (◡𝑆 “ {𝑔})(∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) |
47 | 21, 46 | sylbir 224 |
. . . . . . . . 9
⊢
((∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑟 ∈ (◡𝑆 “ {𝑔})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) |
48 | 16, 20, 47 | syl2anb 495 |
. . . . . . . 8
⊢ ((𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ) → ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) |
49 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 17985 |
. . . . . . . 8
⊢ (𝑓𝐿ℎ ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) |
50 | 48, 49 | sylibr 223 |
. . . . . . 7
⊢ ((𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ) → 𝑓𝐿ℎ) |
51 | 50 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ) |
52 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑎‘0) = (𝑎‘0) |
53 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑎 → (𝑏‘0) = (𝑎‘0)) |
54 | 53 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑎 → ((𝑎‘0) = (𝑏‘0) ↔ (𝑎‘0) = (𝑎‘0))) |
55 | 54 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (◡𝑆 “ {𝑓}) ∧ (𝑎‘0) = (𝑎‘0)) → ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) |
56 | 52, 55 | mpan2 703 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (◡𝑆 “ {𝑓}) → ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) |
57 | 56 | pm4.71i 662 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (◡𝑆 “ {𝑓}) ↔ (𝑎 ∈ (◡𝑆 “ {𝑓}) ∧ ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0))) |
58 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (𝑆 Fn dom 𝑆 → (𝑎 ∈ (◡𝑆 “ {𝑓}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑓))) |
59 | 24, 58 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (◡𝑆 “ {𝑓}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑓)) |
60 | 57, 59 | bitr3i 265 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (◡𝑆 “ {𝑓}) ∧ ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑓)) |
61 | 60 | rexbii2 3021 |
. . . . . . . 8
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓) |
62 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 17985 |
. . . . . . . 8
⊢ (𝑓𝐿𝑓 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) |
63 | | forn 6031 |
. . . . . . . . . . 11
⊢ (𝑆:dom 𝑆–onto→𝑊 → ran 𝑆 = 𝑊) |
64 | 22, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran 𝑆 = 𝑊 |
65 | 64 | eleq2i 2680 |
. . . . . . . . 9
⊢ (𝑓 ∈ ran 𝑆 ↔ 𝑓 ∈ 𝑊) |
66 | | fvelrnb 6153 |
. . . . . . . . . 10
⊢ (𝑆 Fn dom 𝑆 → (𝑓 ∈ ran 𝑆 ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓)) |
67 | 24, 66 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑓 ∈ ran 𝑆 ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓) |
68 | 65, 67 | bitr3i 265 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑊 ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓) |
69 | 61, 62, 68 | 3bitr4ri 292 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓) |
70 | 69 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓)) |
71 | 8, 19, 51, 70 | iserd 7655 |
. . . . 5
⊢ (⊤
→ 𝐿 Er 𝑊) |
72 | 71 | trud 1484 |
. . . 4
⊢ 𝐿 Er 𝑊 |
73 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑎 ∈ 𝑊) |
74 | | foelrn 6286 |
. . . . . . . . . . 11
⊢ ((𝑆:dom 𝑆–onto→𝑊 ∧ 𝑎 ∈ 𝑊) → ∃𝑟 ∈ dom 𝑆 𝑎 = (𝑆‘𝑟)) |
75 | 22, 73, 74 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → ∃𝑟 ∈ dom 𝑆 𝑎 = (𝑆‘𝑟)) |
76 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ dom 𝑆) |
77 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑎 = (𝑆‘𝑟)) |
78 | 77 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑆‘𝑟) = 𝑎) |
79 | | fniniseg 6246 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 Fn dom 𝑆 → (𝑟 ∈ (◡𝑆 “ {𝑎}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑎))) |
80 | 24, 79 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ (◡𝑆 “ {𝑎}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑎)) |
81 | 76, 78, 80 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ (◡𝑆 “ {𝑎})) |
82 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑏 ∈ ran (𝑇‘𝑎)) |
83 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑇‘𝑎) = (𝑇‘(𝑆‘𝑟))) |
84 | 83 | rneqd 5274 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → ran (𝑇‘𝑎) = ran (𝑇‘(𝑆‘𝑟))) |
85 | 82, 84 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑏 ∈ ran (𝑇‘(𝑆‘𝑟))) |
86 | 1, 2, 3, 4, 14, 15 | efgsp1 17973 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ ran (𝑇‘(𝑆‘𝑟))) → (𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆) |
87 | 76, 85, 86 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆) |
88 | 1, 2, 3, 4, 14, 15 | efgsdm 17966 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ dom 𝑆 ↔ (𝑟 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑟‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝑟))(𝑟‘𝑖) ∈ ran (𝑇‘(𝑟‘(𝑖 − 1))))) |
89 | 88 | simp1bi 1069 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ dom 𝑆 → 𝑟 ∈ (Word 𝑊 ∖ {∅})) |
90 | 89 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ (Word 𝑊 ∖ {∅})) |
91 | 90 | eldifad 3552 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ Word 𝑊) |
92 | 1, 2, 3, 4 | efgtf 17958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝑊 → ((𝑇‘𝑎) = (𝑓 ∈ (0...(#‘𝑎)), 𝑔 ∈ (𝐼 × 2𝑜) ↦
(𝑎 splice 〈𝑓, 𝑓, 〈“𝑔(𝑀‘𝑔)”〉〉)) ∧ (𝑇‘𝑎):((0...(#‘𝑎)) × (𝐼 ×
2𝑜))⟶𝑊)) |
93 | 92 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝑊 → (𝑇‘𝑎):((0...(#‘𝑎)) × (𝐼 ×
2𝑜))⟶𝑊) |
94 | | frn 5966 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇‘𝑎):((0...(#‘𝑎)) × (𝐼 ×
2𝑜))⟶𝑊 → ran (𝑇‘𝑎) ⊆ 𝑊) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝑊 → ran (𝑇‘𝑎) ⊆ 𝑊) |
96 | 95 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑏 ∈ 𝑊) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑏 ∈ 𝑊) |
98 | 1, 2, 3, 4, 14, 15 | efgsval2 17969 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ Word 𝑊 ∧ 𝑏 ∈ 𝑊 ∧ (𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆) → (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏) |
99 | 91, 97, 87, 98 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏) |
100 | | fniniseg 6246 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 Fn dom 𝑆 → ((𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏}) ↔ ((𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆 ∧ (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏))) |
101 | 24, 100 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏}) ↔ ((𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆 ∧ (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏)) |
102 | 87, 99, 101 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏})) |
103 | 97 | s1cld 13236 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 〈“𝑏”〉 ∈ Word 𝑊) |
104 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ (Word 𝑊 ∖ {∅}) ↔ (𝑟 ∈ Word 𝑊 ∧ 𝑟 ≠ ∅)) |
105 | | lennncl 13180 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 ∈ Word 𝑊 ∧ 𝑟 ≠ ∅) → (#‘𝑟) ∈
ℕ) |
106 | 104, 105 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ (Word 𝑊 ∖ {∅}) → (#‘𝑟) ∈
ℕ) |
107 | 90, 106 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (#‘𝑟) ∈ ℕ) |
108 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(0..^(#‘𝑟)) ↔
(#‘𝑟) ∈
ℕ) |
109 | 107, 108 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 0 ∈ (0..^(#‘𝑟))) |
110 | | ccatval1 13214 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ Word 𝑊 ∧ 〈“𝑏”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(#‘𝑟))) → ((𝑟 ++ 〈“𝑏”〉)‘0) = (𝑟‘0)) |
111 | 91, 103, 109, 110 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → ((𝑟 ++ 〈“𝑏”〉)‘0) = (𝑟‘0)) |
112 | 111 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0)) |
113 | | fveq1 6102 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑟 ++ 〈“𝑏”〉) → (𝑠‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0)) |
114 | 113 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑟 ++ 〈“𝑏”〉) → ((𝑟‘0) = (𝑠‘0) ↔ (𝑟‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0))) |
115 | 114 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏}) ∧ (𝑟‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0)) → ∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) |
116 | 102, 112,
115 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → ∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) |
117 | 81, 116 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟 ∈ (◡𝑆 “ {𝑎}) ∧ ∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0))) |
118 | 117 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → ((𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟)) → (𝑟 ∈ (◡𝑆 “ {𝑎}) ∧ ∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)))) |
119 | 118 | reximdv2 2997 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → (∃𝑟 ∈ dom 𝑆 𝑎 = (𝑆‘𝑟) → ∃𝑟 ∈ (◡𝑆 “ {𝑎})∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0))) |
120 | 75, 119 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → ∃𝑟 ∈ (◡𝑆 “ {𝑎})∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) |
121 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 17985 |
. . . . . . . . 9
⊢ (𝑎𝐿𝑏 ↔ ∃𝑟 ∈ (◡𝑆 “ {𝑎})∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) |
122 | 120, 121 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑎𝐿𝑏) |
123 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
124 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
125 | 123, 124 | elec 7673 |
. . . . . . . 8
⊢ (𝑏 ∈ [𝑎]𝐿 ↔ 𝑎𝐿𝑏) |
126 | 122, 125 | sylibr 223 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑏 ∈ [𝑎]𝐿) |
127 | 126 | ex 449 |
. . . . . 6
⊢ (𝑎 ∈ 𝑊 → (𝑏 ∈ ran (𝑇‘𝑎) → 𝑏 ∈ [𝑎]𝐿)) |
128 | 127 | ssrdv 3574 |
. . . . 5
⊢ (𝑎 ∈ 𝑊 → ran (𝑇‘𝑎) ⊆ [𝑎]𝐿) |
129 | 128 | rgen 2906 |
. . . 4
⊢
∀𝑎 ∈
𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿 |
130 | | fvex 6113 |
. . . . . . 7
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
131 | 1, 130 | eqeltri 2684 |
. . . . . 6
⊢ 𝑊 ∈ V |
132 | | erex 7653 |
. . . . . 6
⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V)) |
133 | 72, 131, 132 | mp2 9 |
. . . . 5
⊢ 𝐿 ∈ V |
134 | | ereq1 7636 |
. . . . . 6
⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊)) |
135 | | eceq2 7671 |
. . . . . . . 8
⊢ (𝑟 = 𝐿 → [𝑎]𝑟 = [𝑎]𝐿) |
136 | 135 | sseq2d 3596 |
. . . . . . 7
⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑎) ⊆ [𝑎]𝑟 ↔ ran (𝑇‘𝑎) ⊆ [𝑎]𝐿)) |
137 | 136 | ralbidv 2969 |
. . . . . 6
⊢ (𝑟 = 𝐿 → (∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟 ↔ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿)) |
138 | 134, 137 | anbi12d 743 |
. . . . 5
⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿))) |
139 | 133, 138 | elab 3319 |
. . . 4
⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿)) |
140 | 72, 129, 139 | mpbir2an 957 |
. . 3
⊢ 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} |
141 | | intss1 4427 |
. . 3
⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} ⊆ 𝐿) |
142 | 140, 141 | ax-mp 5 |
. 2
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} ⊆ 𝐿 |
143 | 5, 142 | eqsstri 3598 |
1
⊢ ∼
⊆ 𝐿 |