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

Metamath Proof Explorer

Theorem funcnvs2

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

Ref Expression
Assertion funcnvs2 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → Fun ◡ ⟨“ 𝐴 𝐵 ”⟩ )

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1ex ⊢ 1 ∈ V
3 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
4 funcnvpr ⊢ ( ( 0 ∈ V ∧ 1 ∈ V ∧ 𝐴 ≠ 𝐵 ) → Fun ◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
5 1 2 3 4 mp3an12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → Fun ◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
6 s2prop ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
7 6 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
8 7 cnveqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → ◡ ⟨“ 𝐴 𝐵 ”⟩ = ◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
9 8 funeqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → ( Fun ◡ ⟨“ 𝐴 𝐵 ”⟩ ↔ Fun ◡ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) )
10 5 9 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → Fun ◡ ⟨“ 𝐴 𝐵 ”⟩ )