fcnvgreu

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)

		Ref	Expression
	Assertion	fcnvgreu	$⊢ ((Rel A \land Fun A^{-1}) \land Y \in ran A) \to \exists! p \in A Y = 2^{nd} (p)$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$⊢ ran A = dom A^{-1}$
2	1	eleq2i	$⊢ Y \in ran A \leftrightarrow Y \in dom A^{-1}$
3		fgreu	$⊢ (Fun A^{-1} \land Y \in dom A^{-1}) \to \exists! q \in A^{-1} Y = 1^{st} (q)$
4	3	adantll	$⊢ ((Rel A \land Fun A^{-1}) \land Y \in dom A^{-1}) \to \exists! q \in A^{-1} Y = 1^{st} (q)$
5	2 4	sylan2b	$⊢ ((Rel A \land Fun A^{-1}) \land Y \in ran A) \to \exists! q \in A^{-1} Y = 1^{st} (q)$
6		cnvcnvss	$⊢ {A^{-1}}^{-1} \subseteq A$
7		cnvssrndm	$⊢ A^{-1} \subseteq ran A \times dom A$
8	7	sseli	$⊢ q \in A^{-1} \to q \in (ran A \times dom A)$
9		dfdm4	$⊢ dom A = ran A^{-1}$
10	1 9	xpeq12i	$⊢ ran A \times dom A = dom A^{-1} \times ran A^{-1}$
11	8 10	eleqtrdi	$⊢ q \in A^{-1} \to q \in (dom A^{-1} \times ran A^{-1})$
12		2nd1st	$⊢ q \in (dom A^{-1} \times ran A^{-1}) \to ⋃ {\{q\}}^{-1} = ⟨2^{nd} (q), 1^{st} (q)⟩$
13	11 12	syl	$⊢ q \in A^{-1} \to ⋃ {\{q\}}^{-1} = ⟨2^{nd} (q), 1^{st} (q)⟩$
14	13	eqcomd	$⊢ q \in A^{-1} \to ⟨2^{nd} (q), 1^{st} (q)⟩ = ⋃ {\{q\}}^{-1}$
15		relcnv	$⊢ Rel A^{-1}$
16		cnvf1olem	$⊢ (Rel A^{-1} \land (q \in A^{-1} \land ⟨2^{nd} (q), 1^{st} (q)⟩ = ⋃ {\{q\}}^{-1})) \to (⟨2^{nd} (q), 1^{st} (q)⟩ \in {A^{-1}}^{-1} \land q = ⋃ {\{⟨2^{nd} (q), 1^{st} (q)⟩\}}^{-1})$
17	16	simpld	$⊢ (Rel A^{-1} \land (q \in A^{-1} \land ⟨2^{nd} (q), 1^{st} (q)⟩ = ⋃ {\{q\}}^{-1})) \to ⟨2^{nd} (q), 1^{st} (q)⟩ \in {A^{-1}}^{-1}$
18	15 17	mpan	$⊢ (q \in A^{-1} \land ⟨2^{nd} (q), 1^{st} (q)⟩ = ⋃ {\{q\}}^{-1}) \to ⟨2^{nd} (q), 1^{st} (q)⟩ \in {A^{-1}}^{-1}$
19	14 18	mpdan	$⊢ q \in A^{-1} \to ⟨2^{nd} (q), 1^{st} (q)⟩ \in {A^{-1}}^{-1}$
20	6 19	sseldi	$⊢ q \in A^{-1} \to ⟨2^{nd} (q), 1^{st} (q)⟩ \in A$
21	20	adantl	$⊢ ((Rel A \land Fun A^{-1}) \land q \in A^{-1}) \to ⟨2^{nd} (q), 1^{st} (q)⟩ \in A$
22		simpll	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to Rel A$
23		simpr	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to p \in A$
24		relssdmrn	$⊢ Rel A \to A \subseteq dom A \times ran A$
25	24	adantr	$⊢ (Rel A \land Fun A^{-1}) \to A \subseteq dom A \times ran A$
26	25	sselda	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to p \in (dom A \times ran A)$
27		2nd1st	$⊢ p \in (dom A \times ran A) \to ⋃ {\{p\}}^{-1} = ⟨2^{nd} (p), 1^{st} (p)⟩$
28	26 27	syl	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to ⋃ {\{p\}}^{-1} = ⟨2^{nd} (p), 1^{st} (p)⟩$
29	28	eqcomd	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to ⟨2^{nd} (p), 1^{st} (p)⟩ = ⋃ {\{p\}}^{-1}$
30		cnvf1olem	$⊢ (Rel A \land (p \in A \land ⟨2^{nd} (p), 1^{st} (p)⟩ = ⋃ {\{p\}}^{-1})) \to (⟨2^{nd} (p), 1^{st} (p)⟩ \in A^{-1} \land p = ⋃ {\{⟨2^{nd} (p), 1^{st} (p)⟩\}}^{-1})$
31	30	simpld	$⊢ (Rel A \land (p \in A \land ⟨2^{nd} (p), 1^{st} (p)⟩ = ⋃ {\{p\}}^{-1})) \to ⟨2^{nd} (p), 1^{st} (p)⟩ \in A^{-1}$
32	22 23 29 31	syl12anc	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to ⟨2^{nd} (p), 1^{st} (p)⟩ \in A^{-1}$
33	15	a1i	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to Rel A^{-1}$
34		simplr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to q \in A^{-1}$
35	14	ad2antlr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to ⟨2^{nd} (q), 1^{st} (q)⟩ = ⋃ {\{q\}}^{-1}$
36	16	simprd	$⊢ (Rel A^{-1} \land (q \in A^{-1} \land ⟨2^{nd} (q), 1^{st} (q)⟩ = ⋃ {\{q\}}^{-1})) \to q = ⋃ {\{⟨2^{nd} (q), 1^{st} (q)⟩\}}^{-1}$
37	33 34 35 36	syl12anc	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to q = ⋃ {\{⟨2^{nd} (q), 1^{st} (q)⟩\}}^{-1}$
38		simpr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to p = ⟨2^{nd} (q), 1^{st} (q)⟩$
39	38	sneqd	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to \{p\} = \{⟨2^{nd} (q), 1^{st} (q)⟩\}$
40	39	cnveqd	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to {\{p\}}^{-1} = {\{⟨2^{nd} (q), 1^{st} (q)⟩\}}^{-1}$
41	40	unieqd	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to ⋃ {\{p\}}^{-1} = ⋃ {\{⟨2^{nd} (q), 1^{st} (q)⟩\}}^{-1}$
42	28	ad2antrr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to ⋃ {\{p\}}^{-1} = ⟨2^{nd} (p), 1^{st} (p)⟩$
43	37 41 42	3eqtr2d	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to q = ⟨2^{nd} (p), 1^{st} (p)⟩$
44	30	simprd	$⊢ (Rel A \land (p \in A \land ⟨2^{nd} (p), 1^{st} (p)⟩ = ⋃ {\{p\}}^{-1})) \to p = ⋃ {\{⟨2^{nd} (p), 1^{st} (p)⟩\}}^{-1}$
45	22 23 29 44	syl12anc	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to p = ⋃ {\{⟨2^{nd} (p), 1^{st} (p)⟩\}}^{-1}$
46	45	ad2antrr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to p = ⋃ {\{⟨2^{nd} (p), 1^{st} (p)⟩\}}^{-1}$
47		simpr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to q = ⟨2^{nd} (p), 1^{st} (p)⟩$
48	47	sneqd	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to \{q\} = \{⟨2^{nd} (p), 1^{st} (p)⟩\}$
49	48	cnveqd	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to {\{q\}}^{-1} = {\{⟨2^{nd} (p), 1^{st} (p)⟩\}}^{-1}$
50	49	unieqd	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to ⋃ {\{q\}}^{-1} = ⋃ {\{⟨2^{nd} (p), 1^{st} (p)⟩\}}^{-1}$
51	13	ad2antlr	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to ⋃ {\{q\}}^{-1} = ⟨2^{nd} (q), 1^{st} (q)⟩$
52	46 50 51	3eqtr2d	$⊢ ((((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \land q = ⟨2^{nd} (p), 1^{st} (p)⟩) \to p = ⟨2^{nd} (q), 1^{st} (q)⟩$
53	43 52	impbida	$⊢ (((Rel A \land Fun A^{-1}) \land p \in A) \land q \in A^{-1}) \to (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = ⟨2^{nd} (p), 1^{st} (p)⟩)$
54	53	ralrimiva	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to \forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = ⟨2^{nd} (p), 1^{st} (p)⟩)$
55		eqeq2	$⊢ r = ⟨2^{nd} (p), 1^{st} (p)⟩ \to (q = r \leftrightarrow q = ⟨2^{nd} (p), 1^{st} (p)⟩)$
56	55	bibi2d	$⊢ r = ⟨2^{nd} (p), 1^{st} (p)⟩ \to ((p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = r) \leftrightarrow (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = ⟨2^{nd} (p), 1^{st} (p)⟩))$
57	56	ralbidv	$⊢ r = ⟨2^{nd} (p), 1^{st} (p)⟩ \to (\forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = r) \leftrightarrow \forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = ⟨2^{nd} (p), 1^{st} (p)⟩))$
58	57	rspcev	$⊢ (⟨2^{nd} (p), 1^{st} (p)⟩ \in A^{-1} \land \forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = ⟨2^{nd} (p), 1^{st} (p)⟩)) \to \exists r \in A^{-1} \forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = r)$
59	32 54 58	syl2anc	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to \exists r \in A^{-1} \forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = r)$
60		reu6	$⊢ \exists! q \in A^{-1} p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow \exists r \in A^{-1} \forall q \in A^{-1} (p = ⟨2^{nd} (q), 1^{st} (q)⟩ \leftrightarrow q = r)$
61	59 60	sylibr	$⊢ ((Rel A \land Fun A^{-1}) \land p \in A) \to \exists! q \in A^{-1} p = ⟨2^{nd} (q), 1^{st} (q)⟩$
62		fvex	$⊢ 2^{nd} (q) \in V$
63		fvex	$⊢ 1^{st} (q) \in V$
64	62 63	op2ndd	$⊢ p = ⟨2^{nd} (q), 1^{st} (q)⟩ \to 2^{nd} (p) = 1^{st} (q)$
65	64	eqeq2d	$⊢ p = ⟨2^{nd} (q), 1^{st} (q)⟩ \to (Y = 2^{nd} (p) \leftrightarrow Y = 1^{st} (q))$
66	65	adantl	$⊢ ((Rel A \land Fun A^{-1}) \land p = ⟨2^{nd} (q), 1^{st} (q)⟩) \to (Y = 2^{nd} (p) \leftrightarrow Y = 1^{st} (q))$
67	21 61 66	reuxfr1d	$⊢ (Rel A \land Fun A^{-1}) \to (\exists! p \in A Y = 2^{nd} (p) \leftrightarrow \exists! q \in A^{-1} Y = 1^{st} (q))$
68	67	adantr	$⊢ ((Rel A \land Fun A^{-1}) \land Y \in ran A) \to (\exists! p \in A Y = 2^{nd} (p) \leftrightarrow \exists! q \in A^{-1} Y = 1^{st} (q))$
69	5 68	mpbird	$⊢ ((Rel A \land Fun A^{-1}) \land Y \in ran A) \to \exists! p \in A Y = 2^{nd} (p)$

Metamath Proof Explorer

Theorem fcnvgreu

Proof