Metamath Proof Explorer

Theorem bj-restn0

Description: An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restn0 ⊢ X ∈ V ∧ A ∈ W → X ≠ ∅ → X ↾ 𝑡 A ≠ ∅

Proof

Step Hyp Ref Expression
1 n0 ⊢ X ≠ ∅ ↔ ∃ y y ∈ X
2 vex ⊢ y ∈ V
3 2 inex1 ⊢ y ∩ A ∈ V
4 3 isseti ⊢ ∃ x x = y ∩ A
5 4 jctr ⊢ y ∈ X → y ∈ X ∧ ∃ x x = y ∩ A
6 5 eximi ⊢ ∃ y y ∈ X → ∃ y y ∈ X ∧ ∃ x x = y ∩ A
7 df-rex ⊢ ∃ y ∈ X ∃ x x = y ∩ A ↔ ∃ y y ∈ X ∧ ∃ x x = y ∩ A
8 6 7 sylibr ⊢ ∃ y y ∈ X → ∃ y ∈ X ∃ x x = y ∩ A
9 rexcom4 ⊢ ∃ y ∈ X ∃ x x = y ∩ A ↔ ∃ x ∃ y ∈ X x = y ∩ A
10 8 9 sylib ⊢ ∃ y y ∈ X → ∃ x ∃ y ∈ X x = y ∩ A
11 10 a1i ⊢ X ∈ V ∧ A ∈ W → ∃ y y ∈ X → ∃ x ∃ y ∈ X x = y ∩ A
12 1 11 syl5bi ⊢ X ∈ V ∧ A ∈ W → X ≠ ∅ → ∃ x ∃ y ∈ X x = y ∩ A
13 elrest ⊢ X ∈ V ∧ A ∈ W → x ∈ X ↾ 𝑡 A ↔ ∃ y ∈ X x = y ∩ A
14 13 biimprd ⊢ X ∈ V ∧ A ∈ W → ∃ y ∈ X x = y ∩ A → x ∈ X ↾ 𝑡 A
15 14 eximdv ⊢ X ∈ V ∧ A ∈ W → ∃ x ∃ y ∈ X x = y ∩ A → ∃ x x ∈ X ↾ 𝑡 A
16 12 15 syld ⊢ X ∈ V ∧ A ∈ W → X ≠ ∅ → ∃ x x ∈ X ↾ 𝑡 A
17 n0 ⊢ X ↾ 𝑡 A ≠ ∅ ↔ ∃ x x ∈ X ↾ 𝑡 A
18 16 17 syl6ibr ⊢ X ∈ V ∧ A ∈ W → X ≠ ∅ → X ↾ 𝑡 A ≠ ∅