Theorem funcnvs4

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

	Ref	Expression
Assertion	funcnvs4	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → Fun ◡ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ )

Proof

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