Metamath Proof Explorer


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