Theorem cnvf1olem

Description: Lemma for cnvf1o . (Contributed by Mario Carneiro, 27-Apr-2014)

	Ref	Expression
Assertion	cnvf1olem	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to \left(C\in A^{-1}\wedge B=\bigcup {\left\{C\right\}}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		simprr	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to C=\bigcup {\left\{B\right\}}^{-1}$$
2		1st2nd	$$⊢\left(\mathrm{Rel}A\wedge B\in A\right)\to B=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩$$
3	2	adantrr	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to B=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩$$
4	3	sneqd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to \left\{B\right\}=\left\{⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right\}$$
5	4	cnveqd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to {\left\{B\right\}}^{-1}={\left\{⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right\}}^{-1}$$
6	5	unieqd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to \bigcup {\left\{B\right\}}^{-1}=\bigcup {\left\{⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right\}}^{-1}$$
7	1 6	eqtrd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to C=\bigcup {\left\{⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right\}}^{-1}$$
8		opswap	$$⊢\bigcup {\left\{⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right\}}^{-1}=⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩$$
9	7 8	eqtrdi	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to C=⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩$$
10		simprl	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to B\in A$$
11	3 10	eqeltrrd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to ⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\in A$$
12		fvex	$$⊢2^{nd}\left(B\right)\in \mathrm{V}$$
13		fvex	$$⊢1^{st}\left(B\right)\in \mathrm{V}$$
14	12 13	opelcnv	$$⊢⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\in A^{-1}\leftrightarrow ⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\in A$$
15	11 14	sylibr	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to ⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\in A^{-1}$$
16	9 15	eqeltrd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to C\in A^{-1}$$
17		opswap	$$⊢\bigcup {\left\{⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\right\}}^{-1}=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩$$
18	17	eqcomi	$$⊢⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩=\bigcup {\left\{⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\right\}}^{-1}$$
19	9	sneqd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to \left\{C\right\}=\left\{⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\right\}$$
20	19	cnveqd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to {\left\{C\right\}}^{-1}={\left\{⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\right\}}^{-1}$$
21	20	unieqd	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to \bigcup {\left\{C\right\}}^{-1}=\bigcup {\left\{⟨2^{nd}\left(B\right),1^{st}\left(B\right)⟩\right\}}^{-1}$$
22	18 3 21	3eqtr4a	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to B=\bigcup {\left\{C\right\}}^{-1}$$
23	16 22	jca	$$⊢\left(\mathrm{Rel}A\wedge \left(B\in A\wedge C=\bigcup {\left\{B\right\}}^{-1}\right)\right)\to \left(C\in A^{-1}\wedge B=\bigcup {\left\{C\right\}}^{-1}\right)$$