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		simpl	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 𝑅 𝑦 )
7		vex	⊢ 𝑥 ∈ V
8	3 7	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
9	6 8	sylibr	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ◡ 𝑅 𝑥 )
10	5 9	jca	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) )
11	10	eximi	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) )
12	7	eldm	⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 )
13	12	anbi1i	⊢ ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
14		elin	⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ 𝐴 ) )
15		19.41v	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
16	13 14 15	3bitr4i	⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
17	7	elima2	⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) )
18	11 16 17	3imtr4i	⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) → 𝑥 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) )
19	18	ssriv	⊢ ( dom 𝑅 ∩ 𝐴 ) ⊆ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) )