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