| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | efgval.w | . . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 2 |  | efgval.r | . . 3
⊢  ∼ = (
~FG ‘𝐼) | 
| 3 |  | efgval2.m | . . 3
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) | 
| 4 |  | efgval2.t | . . 3
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) | 
| 5 | 1, 2, 3, 4 | efgval2 19743 | . 2
⊢  ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} | 
| 6 |  | efgrelexlem.1 | . . . . . . . 8
⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)} | 
| 7 | 6 | relopabiv 5829 | . . . . . . 7
⊢ Rel 𝐿 | 
| 8 | 7 | a1i 11 | . . . . . 6
⊢ (⊤
→ Rel 𝐿) | 
| 9 |  | simpr 484 | . . . . . . 7
⊢
((⊤ ∧ 𝑓𝐿𝑔) → 𝑓𝐿𝑔) | 
| 10 |  | eqcom 2743 | . . . . . . . . . 10
⊢ ((𝑎‘0) = (𝑏‘0) ↔ (𝑏‘0) = (𝑎‘0)) | 
| 11 | 10 | 2rexbii 3128 | . . . . . . . . 9
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑏‘0) = (𝑎‘0)) | 
| 12 |  | rexcom 3289 | . . . . . . . . 9
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑏‘0) = (𝑎‘0) ↔ ∃𝑏 ∈ (◡𝑆 “ {𝑔})∃𝑎 ∈ (◡𝑆 “ {𝑓})(𝑏‘0) = (𝑎‘0)) | 
| 13 | 11, 12 | bitri 275 | . . . . . . . 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 19768 | . . . . . . . 8
⊢ (𝑓𝐿𝑔 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0)) | 
| 17 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19768 | . . . . . . . 8
⊢ (𝑔𝐿𝑓 ↔ ∃𝑏 ∈ (◡𝑆 “ {𝑔})∃𝑎 ∈ (◡𝑆 “ {𝑓})(𝑏‘0) = (𝑎‘0)) | 
| 18 | 13, 16, 17 | 3bitr4i 303 | . . . . . . 7
⊢ (𝑓𝐿𝑔 ↔ 𝑔𝐿𝑓) | 
| 19 | 9, 18 | sylib 218 | . . . . . 6
⊢
((⊤ ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓) | 
| 20 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19768 | . . . . . . . . 9
⊢ (𝑔𝐿ℎ ↔ ∃𝑟 ∈ (◡𝑆 “ {𝑔})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) | 
| 21 |  | reeanv 3228 | . . . . . . . . . 10
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑟 ∈ (◡𝑆 “ {𝑔})(∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) ↔ (∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑟 ∈ (◡𝑆 “ {𝑔})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0))) | 
| 22 | 1, 2, 3, 4, 14, 15 | efgsfo 19758 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑆:dom 𝑆–onto→𝑊 | 
| 23 |  | fofn 6821 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆:dom 𝑆–onto→𝑊 → 𝑆 Fn dom 𝑆) | 
| 24 | 22, 23 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑆 Fn dom 𝑆 | 
| 25 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 Fn dom 𝑆 → (𝑟 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑔))) | 
| 26 | 24, 25 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑔)) | 
| 27 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 Fn dom 𝑆 → (𝑏 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑔))) | 
| 28 | 24, 27 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (◡𝑆 “ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑔)) | 
| 29 |  | eqtr3 2762 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆‘𝑟) = 𝑔 ∧ (𝑆‘𝑏) = 𝑔) → (𝑆‘𝑟) = (𝑆‘𝑏)) | 
| 30 | 1, 2, 3, 4, 14, 15 | efgred 19767 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = (𝑆‘𝑏)) → (𝑟‘0) = (𝑏‘0)) | 
| 31 | 30 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = (𝑆‘𝑏)) → (𝑏‘0) = (𝑟‘0)) | 
| 32 | 31 | 3expa 1118 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ (𝑆‘𝑟) = (𝑆‘𝑏)) → (𝑏‘0) = (𝑟‘0)) | 
| 33 | 29, 32 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ ((𝑆‘𝑟) = 𝑔 ∧ (𝑆‘𝑏) = 𝑔)) → (𝑏‘0) = (𝑟‘0)) | 
| 34 | 33 | an4s 660 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑔) ∧ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑔)) → (𝑏‘0) = (𝑟‘0)) | 
| 35 | 26, 28, 34 | syl2anb 598 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → (𝑏‘0) = (𝑟‘0)) | 
| 36 |  | eqeq2 2748 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑟‘0) = (𝑠‘0) → ((𝑏‘0) = (𝑟‘0) ↔ (𝑏‘0) = (𝑠‘0))) | 
| 37 | 35, 36 | syl5ibcom 245 | . . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → ((𝑟‘0) = (𝑠‘0) → (𝑏‘0) = (𝑠‘0))) | 
| 38 | 37 | reximdv 3169 | . . . . . . . . . . . . . . 15
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑏‘0) = (𝑠‘0))) | 
| 39 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑎‘0) = (𝑏‘0) → ((𝑎‘0) = (𝑠‘0) ↔ (𝑏‘0) = (𝑠‘0))) | 
| 40 | 39 | rexbidv 3178 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎‘0) = (𝑏‘0) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0) ↔ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑏‘0) = (𝑠‘0))) | 
| 41 | 40 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ ((𝑎‘0) = (𝑏‘0) → ((∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) ↔ (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑏‘0) = (𝑠‘0)))) | 
| 42 | 38, 41 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ (◡𝑆 “ {𝑔}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑔})) → ((𝑎‘0) = (𝑏‘0) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)))) | 
| 43 | 42 | rexlimdva 3154 | . . . . . . . . . . . . 13
⊢ (𝑟 ∈ (◡𝑆 “ {𝑔}) → (∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) → (∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)))) | 
| 44 | 43 | impd 410 | . . . . . . . . . . . 12
⊢ (𝑟 ∈ (◡𝑆 “ {𝑔}) → ((∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0))) | 
| 45 | 44 | rexlimiv 3147 | . . . . . . . . . . 11
⊢
(∃𝑟 ∈
(◡𝑆 “ {𝑔})(∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) | 
| 46 | 45 | reximi 3083 | . . . . . . . . . 10
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑟 ∈ (◡𝑆 “ {𝑔})(∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) | 
| 47 | 21, 46 | sylbir 235 | . . . . . . . . 9
⊢
((∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑔})(𝑎‘0) = (𝑏‘0) ∧ ∃𝑟 ∈ (◡𝑆 “ {𝑔})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑟‘0) = (𝑠‘0)) → ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) | 
| 48 | 16, 20, 47 | syl2anb 598 | . . . . . . . 8
⊢ ((𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ) → ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) | 
| 49 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19768 | . . . . . . . 8
⊢ (𝑓𝐿ℎ ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑠 ∈ (◡𝑆 “ {ℎ})(𝑎‘0) = (𝑠‘0)) | 
| 50 | 48, 49 | sylibr 234 | . . . . . . 7
⊢ ((𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ) → 𝑓𝐿ℎ) | 
| 51 | 50 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ) | 
| 52 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑎‘0) = (𝑎‘0) | 
| 53 |  | fveq1 6904 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑎 → (𝑏‘0) = (𝑎‘0)) | 
| 54 | 53 | rspceeqv 3644 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ (◡𝑆 “ {𝑓}) ∧ (𝑎‘0) = (𝑎‘0)) → ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) | 
| 55 | 52, 54 | mpan2 691 | . . . . . . . . . . 11
⊢ (𝑎 ∈ (◡𝑆 “ {𝑓}) → ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) | 
| 56 | 55 | pm4.71i 559 | . . . . . . . . . 10
⊢ (𝑎 ∈ (◡𝑆 “ {𝑓}) ↔ (𝑎 ∈ (◡𝑆 “ {𝑓}) ∧ ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0))) | 
| 57 |  | fniniseg 7079 | . . . . . . . . . . 11
⊢ (𝑆 Fn dom 𝑆 → (𝑎 ∈ (◡𝑆 “ {𝑓}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑓))) | 
| 58 | 24, 57 | ax-mp 5 | . . . . . . . . . 10
⊢ (𝑎 ∈ (◡𝑆 “ {𝑓}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑓)) | 
| 59 | 56, 58 | bitr3i 277 | . . . . . . . . 9
⊢ ((𝑎 ∈ (◡𝑆 “ {𝑓}) ∧ ∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑓)) | 
| 60 | 59 | rexbii2 3089 | . . . . . . . 8
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓) | 
| 61 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19768 | . . . . . . . 8
⊢ (𝑓𝐿𝑓 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑓})∃𝑏 ∈ (◡𝑆 “ {𝑓})(𝑎‘0) = (𝑏‘0)) | 
| 62 |  | forn 6822 | . . . . . . . . . . 11
⊢ (𝑆:dom 𝑆–onto→𝑊 → ran 𝑆 = 𝑊) | 
| 63 | 22, 62 | ax-mp 5 | . . . . . . . . . 10
⊢ ran 𝑆 = 𝑊 | 
| 64 | 63 | eleq2i 2832 | . . . . . . . . 9
⊢ (𝑓 ∈ ran 𝑆 ↔ 𝑓 ∈ 𝑊) | 
| 65 |  | fvelrnb 6968 | . . . . . . . . . 10
⊢ (𝑆 Fn dom 𝑆 → (𝑓 ∈ ran 𝑆 ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓)) | 
| 66 | 24, 65 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑓 ∈ ran 𝑆 ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓) | 
| 67 | 64, 66 | bitr3i 277 | . . . . . . . 8
⊢ (𝑓 ∈ 𝑊 ↔ ∃𝑎 ∈ dom 𝑆(𝑆‘𝑎) = 𝑓) | 
| 68 | 60, 61, 67 | 3bitr4ri 304 | . . . . . . 7
⊢ (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓) | 
| 69 | 68 | a1i 11 | . . . . . 6
⊢ (⊤
→ (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓)) | 
| 70 | 8, 19, 51, 69 | iserd 8772 | . . . . 5
⊢ (⊤
→ 𝐿 Er 𝑊) | 
| 71 | 70 | mptru 1546 | . . . 4
⊢ 𝐿 Er 𝑊 | 
| 72 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑎 ∈ 𝑊) | 
| 73 |  | foelrn 7126 | . . . . . . . . . . 11
⊢ ((𝑆:dom 𝑆–onto→𝑊 ∧ 𝑎 ∈ 𝑊) → ∃𝑟 ∈ dom 𝑆 𝑎 = (𝑆‘𝑟)) | 
| 74 | 22, 72, 73 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → ∃𝑟 ∈ dom 𝑆 𝑎 = (𝑆‘𝑟)) | 
| 75 |  | simprl 770 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ dom 𝑆) | 
| 76 |  | simprr 772 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑎 = (𝑆‘𝑟)) | 
| 77 | 76 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑆‘𝑟) = 𝑎) | 
| 78 |  | fniniseg 7079 | . . . . . . . . . . . 12
⊢ (𝑆 Fn dom 𝑆 → (𝑟 ∈ (◡𝑆 “ {𝑎}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑎))) | 
| 79 | 24, 78 | ax-mp 5 | . . . . . . . . . . 11
⊢ (𝑟 ∈ (◡𝑆 “ {𝑎}) ↔ (𝑟 ∈ dom 𝑆 ∧ (𝑆‘𝑟) = 𝑎)) | 
| 80 | 75, 77, 79 | sylanbrc 583 | . . . . . . . . . 10
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ (◡𝑆 “ {𝑎})) | 
| 81 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑏 ∈ ran (𝑇‘𝑎)) | 
| 82 | 76 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑇‘𝑎) = (𝑇‘(𝑆‘𝑟))) | 
| 83 | 82 | rneqd 5948 | . . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → ran (𝑇‘𝑎) = ran (𝑇‘(𝑆‘𝑟))) | 
| 84 | 81, 83 | eleqtrd 2842 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑏 ∈ ran (𝑇‘(𝑆‘𝑟))) | 
| 85 | 1, 2, 3, 4, 14, 15 | efgsp1 19756 | . . . . . . . . . . . . 13
⊢ ((𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ ran (𝑇‘(𝑆‘𝑟))) → (𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆) | 
| 86 | 75, 84, 85 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆) | 
| 87 | 1, 2, 3, 4, 14, 15 | efgsdm 19749 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ dom 𝑆 ↔ (𝑟 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑟‘0) ∈ 𝐷 ∧ ∀𝑖 ∈
(1..^(♯‘𝑟))(𝑟‘𝑖) ∈ ran (𝑇‘(𝑟‘(𝑖 − 1))))) | 
| 88 | 87 | simp1bi 1145 | . . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ dom 𝑆 → 𝑟 ∈ (Word 𝑊 ∖ {∅})) | 
| 89 | 88 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ (Word 𝑊 ∖ {∅})) | 
| 90 | 89 | eldifad 3962 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑟 ∈ Word 𝑊) | 
| 91 | 1, 2, 3, 4 | efgtf 19741 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝑊 → ((𝑇‘𝑎) = (𝑓 ∈ (0...(♯‘𝑎)), 𝑔 ∈ (𝐼 × 2o) ↦ (𝑎 splice 〈𝑓, 𝑓, 〈“𝑔(𝑀‘𝑔)”〉〉)) ∧ (𝑇‘𝑎):((0...(♯‘𝑎)) × (𝐼 × 2o))⟶𝑊)) | 
| 92 | 91 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝑊 → (𝑇‘𝑎):((0...(♯‘𝑎)) × (𝐼 × 2o))⟶𝑊) | 
| 93 | 92 | frnd 6743 | . . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ 𝑊 → ran (𝑇‘𝑎) ⊆ 𝑊) | 
| 94 | 93 | sselda 3982 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑏 ∈ 𝑊) | 
| 95 | 94 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 𝑏 ∈ 𝑊) | 
| 96 | 1, 2, 3, 4, 14, 15 | efgsval2 19752 | . . . . . . . . . . . . 13
⊢ ((𝑟 ∈ Word 𝑊 ∧ 𝑏 ∈ 𝑊 ∧ (𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆) → (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏) | 
| 97 | 90, 95, 86, 96 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏) | 
| 98 |  | fniniseg 7079 | . . . . . . . . . . . . 13
⊢ (𝑆 Fn dom 𝑆 → ((𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏}) ↔ ((𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆 ∧ (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏))) | 
| 99 | 24, 98 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ((𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏}) ↔ ((𝑟 ++ 〈“𝑏”〉) ∈ dom 𝑆 ∧ (𝑆‘(𝑟 ++ 〈“𝑏”〉)) = 𝑏)) | 
| 100 | 86, 97, 99 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏})) | 
| 101 | 95 | s1cld 14642 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 〈“𝑏”〉 ∈ Word 𝑊) | 
| 102 |  | eldifsn 4785 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ (Word 𝑊 ∖ {∅}) ↔ (𝑟 ∈ Word 𝑊 ∧ 𝑟 ≠ ∅)) | 
| 103 |  | lennncl 14573 | . . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ Word 𝑊 ∧ 𝑟 ≠ ∅) → (♯‘𝑟) ∈
ℕ) | 
| 104 | 102, 103 | sylbi 217 | . . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ (Word 𝑊 ∖ {∅}) →
(♯‘𝑟) ∈
ℕ) | 
| 105 | 89, 104 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (♯‘𝑟) ∈ ℕ) | 
| 106 |  | lbfzo0 13740 | . . . . . . . . . . . . . 14
⊢ (0 ∈
(0..^(♯‘𝑟))
↔ (♯‘𝑟)
∈ ℕ) | 
| 107 | 105, 106 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → 0 ∈ (0..^(♯‘𝑟))) | 
| 108 |  | ccatval1 14616 | . . . . . . . . . . . . 13
⊢ ((𝑟 ∈ Word 𝑊 ∧ 〈“𝑏”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘𝑟))) → ((𝑟 ++ 〈“𝑏”〉)‘0) = (𝑟‘0)) | 
| 109 | 90, 101, 107, 108 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → ((𝑟 ++ 〈“𝑏”〉)‘0) = (𝑟‘0)) | 
| 110 | 109 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → (𝑟‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0)) | 
| 111 |  | fveq1 6904 | . . . . . . . . . . . 12
⊢ (𝑠 = (𝑟 ++ 〈“𝑏”〉) → (𝑠‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0)) | 
| 112 | 111 | rspceeqv 3644 | . . . . . . . . . . 11
⊢ (((𝑟 ++ 〈“𝑏”〉) ∈ (◡𝑆 “ {𝑏}) ∧ (𝑟‘0) = ((𝑟 ++ 〈“𝑏”〉)‘0)) → ∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) | 
| 113 | 100, 110,
112 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) ∧ (𝑟 ∈ dom 𝑆 ∧ 𝑎 = (𝑆‘𝑟))) → ∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) | 
| 114 | 74, 80, 113 | reximssdv 3172 | . . . . . . . . 9
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → ∃𝑟 ∈ (◡𝑆 “ {𝑎})∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) | 
| 115 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19768 | . . . . . . . . 9
⊢ (𝑎𝐿𝑏 ↔ ∃𝑟 ∈ (◡𝑆 “ {𝑎})∃𝑠 ∈ (◡𝑆 “ {𝑏})(𝑟‘0) = (𝑠‘0)) | 
| 116 | 114, 115 | sylibr 234 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑎𝐿𝑏) | 
| 117 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑏 ∈ V | 
| 118 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑎 ∈ V | 
| 119 | 117, 118 | elec 8792 | . . . . . . . 8
⊢ (𝑏 ∈ [𝑎]𝐿 ↔ 𝑎𝐿𝑏) | 
| 120 | 116, 119 | sylibr 234 | . . . . . . 7
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran (𝑇‘𝑎)) → 𝑏 ∈ [𝑎]𝐿) | 
| 121 | 120 | ex 412 | . . . . . 6
⊢ (𝑎 ∈ 𝑊 → (𝑏 ∈ ran (𝑇‘𝑎) → 𝑏 ∈ [𝑎]𝐿)) | 
| 122 | 121 | ssrdv 3988 | . . . . 5
⊢ (𝑎 ∈ 𝑊 → ran (𝑇‘𝑎) ⊆ [𝑎]𝐿) | 
| 123 | 122 | rgen 3062 | . . . 4
⊢
∀𝑎 ∈
𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿 | 
| 124 | 1 | fvexi 6919 | . . . . . 6
⊢ 𝑊 ∈ V | 
| 125 |  | erex 8770 | . . . . . 6
⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V)) | 
| 126 | 71, 124, 125 | mp2 9 | . . . . 5
⊢ 𝐿 ∈ V | 
| 127 |  | ereq1 8753 | . . . . . 6
⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊)) | 
| 128 |  | eceq2 8787 | . . . . . . . 8
⊢ (𝑟 = 𝐿 → [𝑎]𝑟 = [𝑎]𝐿) | 
| 129 | 128 | sseq2d 4015 | . . . . . . 7
⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑎) ⊆ [𝑎]𝑟 ↔ ran (𝑇‘𝑎) ⊆ [𝑎]𝐿)) | 
| 130 | 129 | ralbidv 3177 | . . . . . 6
⊢ (𝑟 = 𝐿 → (∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟 ↔ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿)) | 
| 131 | 127, 130 | anbi12d 632 | . . . . 5
⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿))) | 
| 132 | 126, 131 | elab 3678 | . . . 4
⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝐿)) | 
| 133 | 71, 123, 132 | mpbir2an 711 | . . 3
⊢ 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} | 
| 134 |  | intss1 4962 | . . 3
⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} ⊆ 𝐿) | 
| 135 | 133, 134 | ax-mp 5 | . 2
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑎 ∈ 𝑊 ran (𝑇‘𝑎) ⊆ [𝑎]𝑟)} ⊆ 𝐿 | 
| 136 | 5, 135 | eqsstri 4029 | 1
⊢  ∼
⊆ 𝐿 |