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	$⊢ (A \in V \land B \in V \land A \neq B) \to Fun {⟨“ A B ”⟩}^{-1}$

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

Metamath Proof Explorer