Step |
Hyp |
Ref |
Expression |
1 |
|
restin.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
uniexg |
⊢ ( 𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V ) |
3 |
1 2
|
eqeltrid |
⊢ ( 𝐽 ∈ 𝑉 → 𝑋 ∈ V ) |
4 |
3
|
adantr |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → 𝑋 ∈ V ) |
5 |
|
restco |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑋 ∈ V ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) ) |
6 |
5
|
3com23 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑋 ∈ V ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) ) |
7 |
4 6
|
mpd3an3 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) ) |
8 |
1
|
restid |
⊢ ( 𝐽 ∈ 𝑉 → ( 𝐽 ↾t 𝑋 ) = 𝐽 ) |
9 |
8
|
adantr |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝑋 ) = 𝐽 ) |
10 |
9
|
oveq1d |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝐽 ↾t 𝑋 ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 ) ) |
11 |
|
incom |
⊢ ( 𝑋 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑋 ) |
12 |
11
|
oveq2i |
⊢ ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) |
13 |
12
|
a1i |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t ( 𝑋 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) ) |
14 |
7 10 13
|
3eqtr3d |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) ) |