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 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → Fun ⁡ ⟨“ ABCD ”⟩ -1

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 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ∧ 3 ∈ V
9 funcnvqp ⊢ 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ∧ 3 ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → Fun ⁡ 0 A 1 B ∪ 2 C 3 D -1
10 8 9 sylan ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → Fun ⁡ 0 A 1 B ∪ 2 C 3 D -1
11 s4prop ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ ABCD ”⟩ = 0 A 1 B ∪ 2 C 3 D
12 11 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → ⟨“ ABCD ”⟩ = 0 A 1 B ∪ 2 C 3 D
13 12 cnveqd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → ⟨“ ABCD ”⟩ -1 = 0 A 1 B ∪ 2 C 3 D -1
14 13 funeqd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → Fun ⁡ ⟨“ ABCD ”⟩ -1 ↔ Fun ⁡ 0 A 1 B ∪ 2 C 3 D -1
15 10 14 mpbird ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D → Fun ⁡ ⟨“ ABCD ”⟩ -1