Metamath Proof Explorer

Theorem bj-restb

Description: An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restb ( 𝑋 ∈ 𝑉 → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 )
2 ssidd ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐴 )
3 1 2 ssind ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ ( 𝐵 ∩ 𝐴 ) )
4 inss2 ⊢ ( 𝐵 ∩ 𝐴 ) ⊆ 𝐴
5 4 a1i ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ∩ 𝐴 ) ⊆ 𝐴 )
6 3 5 eqssd ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( 𝐵 ∩ 𝐴 ) )
7 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋 ) )
8 ineq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
9 8 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 = ( 𝑦 ∩ 𝐴 ) ↔ 𝐴 = ( 𝐵 ∩ 𝐴 ) ) )
10 7 9 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ∈ 𝑋 ∧ 𝐴 = ( 𝑦 ∩ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐴 = ( 𝐵 ∩ 𝐴 ) ) ) )
11 10 spcegv ⊢ ( 𝐵 ∈ 𝑋 → ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 = ( 𝐵 ∩ 𝐴 ) ) → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝐴 = ( 𝑦 ∩ 𝐴 ) ) ) )
12 11 expd ⊢ ( 𝐵 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 = ( 𝐵 ∩ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝐴 = ( 𝑦 ∩ 𝐴 ) ) ) ) )
13 12 pm2.43i ⊢ ( 𝐵 ∈ 𝑋 → ( 𝐴 = ( 𝐵 ∩ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝐴 = ( 𝑦 ∩ 𝐴 ) ) ) )
14 6 13 mpan9 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝐴 = ( 𝑦 ∩ 𝐴 ) ) )
15 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 ∩ 𝐴 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝐴 = ( 𝑦 ∩ 𝐴 ) ) )
16 14 15 sylibr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 ∩ 𝐴 ) )
17 16 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) ) → ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 ∩ 𝐴 ) )
18 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ V )
19 elrest ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ( 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 ∩ 𝐴 ) ) )
20 18 19 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 ∩ 𝐴 ) ) )
21 17 20 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) )
22 21 ex ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ) )