This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dminss

Description: An upper bound for intersection with a domain. Theorem 40 of Suppes p. 66, who calls it "somewhat surprising". (Contributed by NM, 11-Aug-2004)

Ref Expression
Assertion dminss ⊢ dom ⁡ R ∩ A ⊆ R -1 R A

Proof

Step Hyp Ref Expression
1 19.8a ⊢ x ∈ A ∧ x R y → ∃ x x ∈ A ∧ x R y
2 1 ancoms ⊢ x R y ∧ x ∈ A → ∃ x x ∈ A ∧ x R y
3 vex ⊢ y ∈ V
4 3 elima2 ⊢ y ∈ R A ↔ ∃ x x ∈ A ∧ x R y
5 2 4 sylibr ⊢ x R y ∧ x ∈ A → y ∈ R A
6 vex ⊢ x ∈ V
7 3 6 brcnv ⊢ y R -1 x ↔ x R y
8 7 biranri ⊢ x R y ∧ x ∈ A → y R -1 x
9 5 8 jca ⊢ x R y ∧ x ∈ A → y ∈ R A ∧ y R -1 x
10 9 eximi ⊢ ∃ y x R y ∧ x ∈ A → ∃ y y ∈ R A ∧ y R -1 x
11 6 eldm ⊢ x ∈ dom ⁡ R ↔ ∃ y x R y
12 11 anbi1i ⊢ x ∈ dom ⁡ R ∧ x ∈ A ↔ ∃ y x R y ∧ x ∈ A
13 elin ⊢ x ∈ dom ⁡ R ∩ A ↔ x ∈ dom ⁡ R ∧ x ∈ A
14 19.41v ⊢ ∃ y x R y ∧ x ∈ A ↔ ∃ y x R y ∧ x ∈ A
15 12 13 14 3bitr4i ⊢ x ∈ dom ⁡ R ∩ A ↔ ∃ y x R y ∧ x ∈ A
16 6 elima2 ⊢ x ∈ R -1 R A ↔ ∃ y y ∈ R A ∧ y R -1 x
17 10 15 16 3imtr4i ⊢ x ∈ dom ⁡ R ∩ A → x ∈ R -1 R A
18 17 ssriv ⊢ dom ⁡ R ∩ A ⊆ R -1 R A