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