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 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → Fun ⁡ ⟨“ ABC ”⟩ -1

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 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V
6 funcnvtp ⊢ 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → Fun ⁡ 0 A 1 B 2 C -1
7 5 6 sylan ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → Fun ⁡ 0 A 1 B 2 C -1
8 s3tpop ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ = 0 A 1 B 2 C
9 8 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ⟨“ ABC ”⟩ = 0 A 1 B 2 C
10 9 cnveqd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ⟨“ ABC ”⟩ -1 = 0 A 1 B 2 C -1
11 10 funeqd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → Fun ⁡ ⟨“ ABC ”⟩ -1 ↔ Fun ⁡ 0 A 1 B 2 C -1
12 7 11 mpbird ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → Fun ⁡ ⟨“ ABC ”⟩ -1