Metamath Proof Explorer

Theorem funcnvs4

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

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

Proof

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