| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . 5
⊢ 𝑦 ∈ V |
| 2 | 1 | inex1 5317 |
. . . 4
⊢ (𝑦 ∩ 𝐴) ∈ V |
| 3 | | ineq1 4213 |
. . . . 5
⊢ (𝑥 = (𝑦 ∩ 𝐴) → (𝑥 ∩ 𝐵) = ((𝑦 ∩ 𝐴) ∩ 𝐵)) |
| 4 | | inass 4228 |
. . . . 5
⊢ ((𝑦 ∩ 𝐴) ∩ 𝐵) = (𝑦 ∩ (𝐴 ∩ 𝐵)) |
| 5 | 3, 4 | eqtrdi 2793 |
. . . 4
⊢ (𝑥 = (𝑦 ∩ 𝐴) → (𝑥 ∩ 𝐵) = (𝑦 ∩ (𝐴 ∩ 𝐵))) |
| 6 | 2, 5 | abrexco 7264 |
. . 3
⊢ {𝑧 ∣ ∃𝑥 ∈ {𝑤 ∣ ∃𝑦 ∈ 𝐽 𝑤 = (𝑦 ∩ 𝐴)}𝑧 = (𝑥 ∩ 𝐵)} = {𝑧 ∣ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ (𝐴 ∩ 𝐵))} |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) = (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) |
| 8 | 7 | rnmpt 5968 |
. . . . 5
⊢ ran
(𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) = {𝑤 ∣ ∃𝑦 ∈ 𝐽 𝑤 = (𝑦 ∩ 𝐴)} |
| 9 | 8 | mpteq1i 5238 |
. . . 4
⊢ (𝑥 ∈ ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ {𝑤 ∣ ∃𝑦 ∈ 𝐽 𝑤 = (𝑦 ∩ 𝐴)} ↦ (𝑥 ∩ 𝐵)) |
| 10 | 9 | rnmpt 5968 |
. . 3
⊢ ran
(𝑥 ∈ ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↦ (𝑥 ∩ 𝐵)) = {𝑧 ∣ ∃𝑥 ∈ {𝑤 ∣ ∃𝑦 ∈ 𝐽 𝑤 = (𝑦 ∩ 𝐴)}𝑧 = (𝑥 ∩ 𝐵)} |
| 11 | | eqid 2737 |
. . . 4
⊢ (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ (𝐴 ∩ 𝐵))) = (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ (𝐴 ∩ 𝐵))) |
| 12 | 11 | rnmpt 5968 |
. . 3
⊢ ran
(𝑦 ∈ 𝐽 ↦ (𝑦 ∩ (𝐴 ∩ 𝐵))) = {𝑧 ∣ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ (𝐴 ∩ 𝐵))} |
| 13 | 6, 10, 12 | 3eqtr4i 2775 |
. 2
⊢ ran
(𝑥 ∈ ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↦ (𝑥 ∩ 𝐵)) = ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ (𝐴 ∩ 𝐵))) |
| 14 | | restval 17471 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴))) |
| 15 | 14 | 3adant3 1133 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴))) |
| 16 | 15 | oveq1d 7446 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↾t 𝐵)) |
| 17 | | ovex 7464 |
. . . . 5
⊢ (𝐽 ↾t 𝐴) ∈ V |
| 18 | 15, 17 | eqeltrrdi 2850 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ∈ V) |
| 19 | | simp3 1139 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
| 20 | | restval 17471 |
. . . 4
⊢ ((ran
(𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ∈ V ∧ 𝐵 ∈ 𝑋) → (ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↾t 𝐵) = ran (𝑥 ∈ ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↦ (𝑥 ∩ 𝐵))) |
| 21 | 18, 19, 20 | syl2anc 584 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↾t 𝐵) = ran (𝑥 ∈ ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↦ (𝑥 ∩ 𝐵))) |
| 22 | 16, 21 | eqtrd 2777 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = ran (𝑥 ∈ ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ 𝐴)) ↦ (𝑥 ∩ 𝐵))) |
| 23 | | simp1 1137 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → 𝐽 ∈ 𝑉) |
| 24 | | inex1g 5319 |
. . . 4
⊢ (𝐴 ∈ 𝑊 → (𝐴 ∩ 𝐵) ∈ V) |
| 25 | 24 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ V) |
| 26 | | restval 17471 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝐽 ↾t (𝐴 ∩ 𝐵)) = ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ (𝐴 ∩ 𝐵)))) |
| 27 | 23, 25, 26 | syl2anc 584 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐽 ↾t (𝐴 ∩ 𝐵)) = ran (𝑦 ∈ 𝐽 ↦ (𝑦 ∩ (𝐴 ∩ 𝐵)))) |
| 28 | 13, 22, 27 | 3eqtr4a 2803 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (𝐽 ↾t (𝐴 ∩ 𝐵))) |