Theorem fcnvgreu 28265

Description: If the converse of a relation A is a function, exactly one point of its graph has a given second element (that is, function value) (Contributed by Thierry Arnoux, 1-Apr-2018.)

Assertion

Ref	Expression
fcnvgreu	|- ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> E! p e. A Y = ( 2nd ` p ) )

Distinct variable groups:   A, p   Y, p

Proof of Theorem fcnvgreu

Dummy variables q r are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rn 4861	. . . 4 |- ran A = dom `' A
2	1	eleq2i 2500	. . 3 |- ( Y e. ran A <-> Y e. dom `' A )
3		fgreu 28264	. . . 4 |- ( ( Fun `' A /\ Y e. dom `' A ) -> E! q e. `' A Y = ( 1st ` q ) )
4	3	adantll 718	. . 3 |- ( ( ( Rel A /\ Fun `' A ) /\ Y e. dom `' A ) -> E! q e. `' A Y = ( 1st ` q ) )
5	2, 4	sylan2b 477	. 2 |- ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> E! q e. `' A Y = ( 1st ` q ) )
6		cnvcnvss 5306	. . . . . 6 |- `' `' A C_ A
7		cnvssrndm 5373	. . . . . . . . . . 11 |- `' A C_ ( ran A X. dom A )
8	7	sseli 3460	. . . . . . . . . 10 |- ( q e. `' A -> q e. ( ran A X. dom A ) )
9		dfdm4 5043	. . . . . . . . . . 11 |- dom A = ran `' A
10	1, 9	xpeq12i 4872	. . . . . . . . . 10 |- ( ran A X. dom A ) = ( dom `' A X. ran `' A )
11	8, 10	syl6eleq 2520	. . . . . . . . 9 |- ( q e. `' A -> q e. ( dom `' A X. ran `' A ) )
12		2nd1st 6849	. . . . . . . . 9 |- ( q e. ( dom `' A X. ran `' A ) -> U. `' { q } = <. ( 2nd ` q ) , ( 1st ` q ) >. )
13	11, 12	syl 17	. . . . . . . 8 |- ( q e. `' A -> U. `' { q } = <. ( 2nd ` q ) , ( 1st ` q ) >. )
14	13	eqcomd 2430	. . . . . . 7 |- ( q e. `' A -> <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } )
15		relcnv 5223	. . . . . . . 8 |- Rel `' A
16		cnvf1olem 6902	. . . . . . . . 9 |- ( ( Rel `' A /\ ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) ) -> ( <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A /\ q = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } ) )
17	16	simpld 460	. . . . . . . 8 |- ( ( Rel `' A /\ ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A )
18	15, 17	mpan 674	. . . . . . 7 |- ( ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A )
19	14, 18	mpdan 672	. . . . . 6 |- ( q e. `' A -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A )
20	6, 19	sseldi 3462	. . . . 5 |- ( q e. `' A -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. A )
21	20	adantl 467	. . . 4 |- ( ( ( Rel A /\ Fun `' A ) /\ q e. `' A ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. A )
22		simpll 758	. . . . . . 7 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> Rel A )
23		simpr 462	. . . . . . 7 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> p e. A )
24		relssdmrn 5372	. . . . . . . . . . 11 |- ( Rel A -> A C_ ( dom A X. ran A ) )
25	24	adantr 466	. . . . . . . . . 10 |- ( ( Rel A /\ Fun `' A ) -> A C_ ( dom A X. ran A ) )
26	25	sselda 3464	. . . . . . . . 9 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> p e. ( dom A X. ran A ) )
27		2nd1st 6849	. . . . . . . . 9 |- ( p e. ( dom A X. ran A ) -> U. `' { p } = <. ( 2nd ` p ) , ( 1st ` p ) >. )
28	26, 27	syl 17	. . . . . . . 8 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> U. `' { p } = <. ( 2nd ` p ) , ( 1st ` p ) >. )
29	28	eqcomd 2430	. . . . . . 7 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } )
30		cnvf1olem 6902	. . . . . . . 8 |- ( ( Rel A /\ ( p e. A /\ <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } ) ) -> ( <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A /\ p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } ) )
31	30	simpld 460	. . . . . . 7 |- ( ( Rel A /\ ( p e. A /\ <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } ) ) -> <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A )
32	22, 23, 29, 31	syl12anc 1262	. . . . . 6 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A )
33	15	a1i 11	. . . . . . . . . 10 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> Rel `' A )
34		simplr 760	. . . . . . . . . 10 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> q e. `' A )
35	14	ad2antlr 731	. . . . . . . . . 10 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } )
36	16	simprd 464	. . . . . . . . . 10 |- ( ( Rel `' A /\ ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) ) -> q = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
37	33, 34, 35, 36	syl12anc 1262	. . . . . . . . 9 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> q = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
38		simpr 462	. . . . . . . . . . . 12 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> p = <. ( 2nd ` q ) , ( 1st ` q ) >. )
39	38	sneqd 4008	. . . . . . . . . . 11 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> { p } = { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
40	39	cnveqd 5026	. . . . . . . . . 10 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> `' { p } = `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
41	40	unieqd 4226	. . . . . . . . 9 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> U. `' { p } = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
42	28	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> U. `' { p } = <. ( 2nd ` p ) , ( 1st ` p ) >. )
43	37, 41, 42	3eqtr2d 2469	. . . . . . . 8 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> q = <. ( 2nd ` p ) , ( 1st ` p ) >. )
44	30	simprd 464	. . . . . . . . . . 11 |- ( ( Rel A /\ ( p e. A /\ <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } ) ) -> p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
45	22, 23, 29, 44	syl12anc 1262	. . . . . . . . . 10 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
46	45	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
47		simpr 462	. . . . . . . . . . . 12 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> q = <. ( 2nd ` p ) , ( 1st ` p ) >. )
48	47	sneqd 4008	. . . . . . . . . . 11 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> { q } = { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
49	48	cnveqd 5026	. . . . . . . . . 10 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> `' { q } = `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
50	49	unieqd 4226	. . . . . . . . 9 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> U. `' { q } = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
51	13	ad2antlr 731	. . . . . . . . 9 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> U. `' { q } = <. ( 2nd ` q ) , ( 1st ` q ) >. )
52	46, 50, 51	3eqtr2d 2469	. . . . . . . 8 |- ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> p = <. ( 2nd ` q ) , ( 1st ` q ) >. )
53	43, 52	impbida 840	. . . . . . 7 |- ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) -> ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) )
54	53	ralrimiva 2839	. . . . . 6 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) )
55		eqeq2 2437	. . . . . . . . 9 |- ( r = <. ( 2nd ` p ) , ( 1st ` p ) >. -> ( q = r <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) )
56	55	bibi2d 319	. . . . . . . 8 |- ( r = <. ( 2nd ` p ) , ( 1st ` p ) >. -> ( ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) <-> ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) ) )
57	56	ralbidv 2864	. . . . . . 7 |- ( r = <. ( 2nd ` p ) , ( 1st ` p ) >. -> ( A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) <-> A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) ) )
58	57	rspcev 3182	. . . . . 6 |- ( ( <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A /\ A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) ) -> E. r e. `' A A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) )
59	32, 54, 58	syl2anc 665	. . . . 5 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> E. r e. `' A A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) )
60		reu6 3260	. . . . 5 |- ( E! q e. `' A p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> E. r e. `' A A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) )
61	59, 60	sylibr 215	. . . 4 |- ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> E! q e. `' A p = <. ( 2nd ` q ) , ( 1st ` q ) >. )
62		fvex 5888	. . . . . . 7 |- ( 2nd ` q ) e. _V
63		fvex 5888	. . . . . . 7 |- ( 1st ` q ) e. _V
64	62, 63	op2ndd 6815	. . . . . 6 |- ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. -> ( 2nd ` p ) = ( 1st ` q ) )
65	64	eqeq2d 2436	. . . . 5 |- ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. -> ( Y = ( 2nd ` p ) <-> Y = ( 1st ` q ) ) )
66	65	adantl 467	. . . 4 |- ( ( ( Rel A /\ Fun `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> ( Y = ( 2nd ` p ) <-> Y = ( 1st ` q ) ) )
67	21, 61, 66	reuxfr4d 28112	. . 3 |- ( ( Rel A /\ Fun `' A ) -> ( E! p e. A Y = ( 2nd ` p ) <-> E! q e. `' A Y = ( 1st ` q ) ) )
68	67	adantr 466	. 2 |- ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> ( E! p e. A Y = ( 2nd ` p ) <-> E! q e. `' A Y = ( 1st ` q ) ) )
69	5, 68	mpbird 235	1 |- ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> E! p e. A Y = ( 2nd ` p ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1868   A.wral 2775   E.wrex 2776   E!wreu 2777   C_ wss 3436   {csn 3996   <.cop 4002   U.cuni 4216   X. cxp 4848   `'ccnv 4849   dom cdm 4850   ran crn 4851   Rel wrel 4855   Fun wfun 5592   ` cfv 5598   1stc1st 6802   2ndc2nd 6803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-iota 5562  df-fun 5600  df-fn 5601  df-fv 5606  df-1st 6804  df-2nd 6805

This theorem is referenced by:  gsummpt2co  28538