| Step | Hyp | Ref
| Expression |
| 1 | | efgval.w |
. . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
| 2 | | efgval.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
| 3 | 1, 2 | efgval 19735 |
. 2
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} |
| 4 | | efgval2.m |
. . . . . . . . . . 11
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
| 5 | | efgval2.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
| 6 | 1, 2, 4, 5 | efgtf 19740 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑊 → ((𝑇‘𝑥) = (𝑚 ∈ (0...(♯‘𝑥)), 𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) ∧ (𝑇‘𝑥):((0...(♯‘𝑥)) × (𝐼 × 2o))⟶𝑊)) |
| 7 | 6 | simpld 494 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → (𝑇‘𝑥) = (𝑚 ∈ (0...(♯‘𝑥)), 𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))) |
| 8 | 7 | rneqd 5949 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑊 → ran (𝑇‘𝑥) = ran (𝑚 ∈ (0...(♯‘𝑥)), 𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))) |
| 9 | 8 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑊 → (ran (𝑇‘𝑥) ⊆ [𝑥]𝑟 ↔ ran (𝑚 ∈ (0...(♯‘𝑥)), 𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) ⊆ [𝑥]𝑟)) |
| 10 | | dfss3 3972 |
. . . . . . . 8
⊢ (ran
(𝑚 ∈
(0...(♯‘𝑥)),
𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) ⊆ [𝑥]𝑟 ↔ ∀𝑎 ∈ ran (𝑚 ∈ (0...(♯‘𝑥)), 𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))𝑎 ∈ [𝑥]𝑟) |
| 11 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ∈
V |
| 12 | 11 | rgen2w 3066 |
. . . . . . . . . 10
⊢
∀𝑚 ∈
(0...(♯‘𝑥))∀𝑢 ∈ (𝐼 × 2o)(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ∈
V |
| 13 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(0...(♯‘𝑥)),
𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) = (𝑚 ∈ (0...(♯‘𝑥)), 𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) |
| 14 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
| 15 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 16 | 14, 15 | elec 8791 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ [𝑥]𝑟 ↔ 𝑥𝑟𝑎) |
| 17 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) → (𝑥𝑟𝑎 ↔ 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))) |
| 18 | 16, 17 | bitrid 283 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) → (𝑎 ∈ [𝑥]𝑟 ↔ 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))) |
| 19 | 13, 18 | ralrnmpo 7572 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
(0...(♯‘𝑥))∀𝑢 ∈ (𝐼 × 2o)(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ∈ V →
(∀𝑎 ∈ ran
(𝑚 ∈
(0...(♯‘𝑥)),
𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))𝑎 ∈ [𝑥]𝑟 ↔ ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑢 ∈ (𝐼 × 2o)𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))) |
| 20 | 12, 19 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
ran (𝑚 ∈
(0...(♯‘𝑥)),
𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))𝑎 ∈ [𝑥]𝑟 ↔ ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑢 ∈ (𝐼 × 2o)𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) |
| 21 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 〈𝑎, 𝑏〉 → 𝑢 = 〈𝑎, 𝑏〉) |
| 22 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 〈𝑎, 𝑏〉 → (𝑀‘𝑢) = (𝑀‘〈𝑎, 𝑏〉)) |
| 23 | | df-ov 7434 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎𝑀𝑏) = (𝑀‘〈𝑎, 𝑏〉) |
| 24 | 22, 23 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 〈𝑎, 𝑏〉 → (𝑀‘𝑢) = (𝑎𝑀𝑏)) |
| 25 | 21, 24 | s2eqd 14902 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 〈𝑎, 𝑏〉 → 〈“𝑢(𝑀‘𝑢)”〉 = 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉) |
| 26 | 25 | oteq3d 4887 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 〈𝑎, 𝑏〉 → 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉 = 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 〈𝑎, 𝑏〉 → (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) = (𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉)) |
| 28 | 27 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑢 = 〈𝑎, 𝑏〉 → (𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ↔ 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉))) |
| 29 | 28 | ralxp 5852 |
. . . . . . . . . . 11
⊢
(∀𝑢 ∈
(𝐼 ×
2o)𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ↔ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉)) |
| 30 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → 〈𝑎, 𝑏〉 = 〈𝑎, 𝑏〉) |
| 31 | 4 | efgmval 19730 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑎𝑀𝑏) = 〈𝑎, (1o ∖ 𝑏)〉) |
| 32 | 30, 31 | s2eqd 14902 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) →
〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉 = 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) |
| 33 | 32 | oteq3d 4887 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉 = 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) |
| 34 | 33 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉) = (𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 35 | 34 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉) ↔ 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 36 | 35 | ralbidva 3176 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐼 → (∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉) ↔ ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 37 | 36 | ralbiia 3091 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉(𝑎𝑀𝑏)”〉〉) ↔ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 38 | 29, 37 | bitri 275 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
(𝐼 ×
2o)𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ↔ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 39 | 38 | ralbii 3093 |
. . . . . . . . 9
⊢
(∀𝑚 ∈
(0...(♯‘𝑥))∀𝑢 ∈ (𝐼 × 2o)𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉) ↔ ∀𝑚 ∈
(0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 40 | 20, 39 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑎 ∈
ran (𝑚 ∈
(0...(♯‘𝑥)),
𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉))𝑎 ∈ [𝑥]𝑟 ↔ ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 41 | 10, 40 | bitri 275 |
. . . . . . 7
⊢ (ran
(𝑚 ∈
(0...(♯‘𝑥)),
𝑢 ∈ (𝐼 × 2o) ↦ (𝑥 splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) ⊆ [𝑥]𝑟 ↔ ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 42 | 9, 41 | bitrdi 287 |
. . . . . 6
⊢ (𝑥 ∈ 𝑊 → (ran (𝑇‘𝑥) ⊆ [𝑥]𝑟 ↔ ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 43 | 42 | ralbiia 3091 |
. . . . 5
⊢
(∀𝑥 ∈
𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟 ↔ ∀𝑥 ∈ 𝑊 ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 44 | 43 | anbi2i 623 |
. . . 4
⊢ ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟) ↔ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 45 | 44 | abbii 2809 |
. . 3
⊢ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟)} = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} |
| 46 | 45 | inteqi 4950 |
. 2
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟)} = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑚 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑚, 𝑚, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} |
| 47 | 3, 46 | eqtr4i 2768 |
1
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟)} |