This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ^◡ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		c0ex	⊢ 0 ∈ V
2		1ex	⊢ 1 ∈ V
3		2ex	⊢ 2 ∈ V
4	1 2 3	3pm3.2i	⊢ ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V )
5	4	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) )
6		funcnvtp	⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ^◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
7	5 6	sylan	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ^◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
8		s3tpop	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
9	8	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
10	9	cnveqd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ^◡ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ^◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } )
11	10	funeqd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( Fun ^◡ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ Fun ^◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , 𝐶 ⟩ } ) )
12	7 11	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ^◡ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )