Metamath Proof Explorer

Theorem funcnvs3

Description: The converse of a length 3 word is a function if its symbols are different sets. (Contributed by Alexander van der Vekens, 31-Jan-2018) (Revised by AV, 23-Jan-2021)

		Ref	Expression
	Assertion	funcnvs3	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to Fun {⟨“ A B C ”⟩}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$⊢ 0 \in V$
2		1ex	$⊢ 1 \in V$
3		2ex	$⊢ 2 \in V$
4	1 2 3	3pm3.2i	$⊢ (0 \in V \land 1 \in V \land 2 \in V)$
5	4	a1i	$⊢ (A \in V \land B \in V \land C \in V) \to (0 \in V \land 1 \in V \land 2 \in V)$
6		funcnvtp	$⊢ ((0 \in V \land 1 \in V \land 2 \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to Fun {\{⟨0, A⟩, ⟨1, B⟩, ⟨2, C⟩\}}^{-1}$
7	5 6	sylan	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to Fun {\{⟨0, A⟩, ⟨1, B⟩, ⟨2, C⟩\}}^{-1}$
8		s3tpop	$⊢ (A \in V \land B \in V \land C \in V) \to ⟨“ A B C ”⟩ = \{⟨0, A⟩, ⟨1, B⟩, ⟨2, C⟩\}$
9	8	adantr	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to ⟨“ A B C ”⟩ = \{⟨0, A⟩, ⟨1, B⟩, ⟨2, C⟩\}$
10	9	cnveqd	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to {⟨“ A B C ”⟩}^{-1} = {\{⟨0, A⟩, ⟨1, B⟩, ⟨2, C⟩\}}^{-1}$
11	10	funeqd	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to (Fun {⟨“ A B C ”⟩}^{-1} \leftrightarrow Fun {\{⟨0, A⟩, ⟨1, B⟩, ⟨2, C⟩\}}^{-1})$
12	7 11	mpbird	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to Fun {⟨“ A B C ”⟩}^{-1}$