Theorem ssrelrn

Description: If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020)

	Ref	Expression
Assertion	ssrelrn	⊢ ( ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑌 ∈ ran 𝑅 ) → ∃ 𝑎 ∈ 𝐴 𝑎 𝑅 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		elrng	⊢ ( 𝑌 ∈ ran 𝑅 → ( 𝑌 ∈ ran 𝑅 ↔ ∃ 𝑎 𝑎 𝑅 𝑌 ) )
2		ssbr	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑎 𝑅 𝑌 → 𝑎 ( 𝐴 × 𝐵 ) 𝑌 ) )
3		brxp	⊢ ( 𝑎 ( 𝐴 × 𝐵 ) 𝑌 ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
4	3	simplbi	⊢ ( 𝑎 ( 𝐴 × 𝐵 ) 𝑌 → 𝑎 ∈ 𝐴 )
5	2 4	syl6	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑎 𝑅 𝑌 → 𝑎 ∈ 𝐴 ) )
6	5	ancrd	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑎 𝑅 𝑌 → ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) )
7	6	adantl	⊢ ( ( 𝑌 ∈ ran 𝑅 ∧ 𝑅 ⊆ ( 𝐴 × 𝐵 ) ) → ( 𝑎 𝑅 𝑌 → ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) )
8	7	eximdv	⊢ ( ( 𝑌 ∈ ran 𝑅 ∧ 𝑅 ⊆ ( 𝐴 × 𝐵 ) ) → ( ∃ 𝑎 𝑎 𝑅 𝑌 → ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) )
9	8	ex	⊢ ( 𝑌 ∈ ran 𝑅 → ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( ∃ 𝑎 𝑎 𝑅 𝑌 → ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) ) )
10	9	com23	⊢ ( 𝑌 ∈ ran 𝑅 → ( ∃ 𝑎 𝑎 𝑅 𝑌 → ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) ) )
11	1 10	sylbid	⊢ ( 𝑌 ∈ ran 𝑅 → ( 𝑌 ∈ ran 𝑅 → ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) ) )
12	11	pm2.43i	⊢ ( 𝑌 ∈ ran 𝑅 → ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) ) )
13	12	impcom	⊢ ( ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑌 ∈ ran 𝑅 ) → ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) )
14		df-rex	⊢ ( ∃ 𝑎 ∈ 𝐴 𝑎 𝑅 𝑌 ↔ ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑎 𝑅 𝑌 ) )
15	13 14	sylibr	⊢ ( ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑌 ∈ ran 𝑅 ) → ∃ 𝑎 ∈ 𝐴 𝑎 𝑅 𝑌 )