Theorem funcnvs2

Description: The converse of a length 2 word is a function if its symbols are different sets. (Contributed by AV, 23-Jan-2021)

	Ref	Expression
Assertion	funcnvs2	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \mathrm{Fun}{⟨“AB”⟩}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$$⊢0\in \mathrm{V}$$
2		1ex	$$⊢1\in \mathrm{V}$$
3		simp3	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to A\ne B$$
4		funcnvpr	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\wedge A\ne B\right)\to \mathrm{Fun}{\left\{⟨0,A⟩,⟨1,B⟩\right\}}^{-1}$$
5	1 2 3 4	mp3an12i	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \mathrm{Fun}{\left\{⟨0,A⟩,⟨1,B⟩\right\}}^{-1}$$
6		s2prop	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“AB”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
7	6	3adant3	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to ⟨“AB”⟩=\left\{⟨0,A⟩,⟨1,B⟩\right\}$$
8	7	cnveqd	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to {⟨“AB”⟩}^{-1}={\left\{⟨0,A⟩,⟨1,B⟩\right\}}^{-1}$$
9	8	funeqd	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\mathrm{Fun}{⟨“AB”⟩}^{-1}\leftrightarrow \mathrm{Fun}{\left\{⟨0,A⟩,⟨1,B⟩\right\}}^{-1}\right)$$
10	5 9	mpbird	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \mathrm{Fun}{⟨“AB”⟩}^{-1}$$