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 𝑅 ∩ 𝐴 ) ⊆ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
2	1	ancoms	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
3		vex	⊢ 𝑦 ∈ V
4	3	elima2	⊢ ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
5	2 4	sylibr	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ( 𝑅 “ 𝐴 ) )
6		vex	⊢ 𝑥 ∈ V
7	3 6	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
8	7	biranri	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ◡ 𝑅 𝑥 )
9	5 8	jca	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) )
10	9	eximi	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) )
11	6	eldm	⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 )
12	11	anbi1i	⊢ ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
13		elin	⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ 𝐴 ) )
14		19.41v	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
15	12 13 14	3bitr4i	⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
16	6	elima2	⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) )
17	10 15 16	3imtr4i	⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) → 𝑥 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) )
18	17	ssriv	⊢ ( dom 𝑅 ∩ 𝐴 ) ⊆ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) )