Theorem ssrelrn 4875

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.)

Assertion

Ref	Expression
ssrelrn	|- ( ( R C_ ( A X. B ) /\ Y e. ran R ) -> E. a e. A a R Y )

Distinct variable groups:   A, a   B, a   R, a   Y, a

Proof of Theorem ssrelrn

Step	Hyp	Ref	Expression
1		elrng 4874	. . . . 5 |- ( Y e. ran R -> ( Y e. ran R <-> E. a a R Y ) )
2		ssbr 4092	. . . . . . . . . . 11 |- ( R C_ ( A X. B ) -> ( a R Y -> a ( A X. B ) Y ) )
3		brxp 4711	. . . . . . . . . . . 12 |- ( a ( A X. B ) Y <-> ( a e. A /\ Y e. B ) )
4	3	simplbi 274	. . . . . . . . . . 11 |- ( a ( A X. B ) Y -> a e. A )
5	2, 4	syl6 33	. . . . . . . . . 10 |- ( R C_ ( A X. B ) -> ( a R Y -> a e. A ) )
6	5	ancrd 326	. . . . . . . . 9 |- ( R C_ ( A X. B ) -> ( a R Y -> ( a e. A /\ a R Y ) ) )
7	6	adantl 277	. . . . . . . 8 |- ( ( Y e. ran R /\ R C_ ( A X. B ) ) -> ( a R Y -> ( a e. A /\ a R Y ) ) )
8	7	eximdv 1904	. . . . . . 7 |- ( ( Y e. ran R /\ R C_ ( A X. B ) ) -> ( E. a a R Y -> E. a ( a e. A /\ a R Y ) ) )
9	8	ex 115	. . . . . 6 |- ( Y e. ran R -> ( R C_ ( A X. B ) -> ( E. a a R Y -> E. a ( a e. A /\ a R Y ) ) ) )
10	9	com23 78	. . . . 5 |- ( Y e. ran R -> ( E. a a R Y -> ( R C_ ( A X. B ) -> E. a ( a e. A /\ a R Y ) ) ) )
11	1, 10	sylbid 150	. . . 4 |- ( Y e. ran R -> ( Y e. ran R -> ( R C_ ( A X. B ) -> E. a ( a e. A /\ a R Y ) ) ) )
12	11	pm2.43i 49	. . 3 |- ( Y e. ran R -> ( R C_ ( A X. B ) -> E. a ( a e. A /\ a R Y ) ) )
13	12	impcom 125	. 2 |- ( ( R C_ ( A X. B ) /\ Y e. ran R ) -> E. a ( a e. A /\ a R Y ) )
14		df-rex 2491	. 2 |- ( E. a e. A a R Y <-> E. a ( a e. A /\ a R Y ) )
15	13, 14	sylibr 134	1 |- ( ( R C_ ( A X. B ) /\ Y e. ran R ) -> E. a e. A a R Y )

Syntax hints:   -> wi 4   /\ wa 104   E.wex 1516   e. wcel 2177   E.wrex 2486   C_ wss 3168   class class class wbr 4048   X. cxp 4678   ran crn 4681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644  df-br 4049  df-opab 4111  df-xp 4686  df-cnv 4688  df-dm 4690  df-rn 4691

This theorem is referenced by:  incistruhgr  15736