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 simpl ⊢ x R y ∧ x ∈ A → x R y
7 vex ⊢ x ∈ V
8 3 7 brcnv ⊢ y R -1 x ↔ x R y
9 6 8 sylibr ⊢ x R y ∧ x ∈ A → y R -1 x
10 5 9 jca ⊢ x R y ∧ x ∈ A → y ∈ R A ∧ y R -1 x
11 10 eximi ⊢ ∃ y x R y ∧ x ∈ A → ∃ y y ∈ R A ∧ y R -1 x
12 7 eldm ⊢ x ∈ dom ⁡ R ↔ ∃ y x R y
13 12 anbi1i ⊢ x ∈ dom ⁡ R ∧ x ∈ A ↔ ∃ y x R y ∧ x ∈ A
14 elin ⊢ x ∈ dom ⁡ R ∩ A ↔ x ∈ dom ⁡ R ∧ x ∈ A
15 19.41v ⊢ ∃ y x R y ∧ x ∈ A ↔ ∃ y x R y ∧ x ∈ A
16 13 14 15 3bitr4i ⊢ x ∈ dom ⁡ R ∩ A ↔ ∃ y x R y ∧ x ∈ A
17 7 elima2 ⊢ x ∈ R -1 R A ↔ ∃ y y ∈ R A ∧ y R -1 x
18 11 16 17 3imtr4i ⊢ x ∈ dom ⁡ R ∩ A → x ∈ R -1 R A
19 18 ssriv ⊢ dom ⁡ R ∩ A ⊆ R -1 R A