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 ⟨“ 𝐴 𝐵 𝐶 ”⟩ )