Metamath Proof Explorer

Theorem s7f1o

Description: A length 7 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by AV, 2-Aug-2025)

Ref Expression
Assertion s7f1o ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → K = ⟨“ ABCDEFG ”⟩ → K : 0 ..^ 7 ⟶ 1-1 onto A B C ∪ D ∪ E F G

Proof

Step Hyp Ref Expression
1 s7cli ⊢ ⟨“ ABCDEFG ”⟩ ∈ Word V
2 wrdf ⊢ ⟨“ ABCDEFG ”⟩ ∈ Word V → ⟨“ ABCDEFG ”⟩ : 0 ..^ ⟨“ ABCDEFG ”⟩ ⟶ V
3 s7len ⊢ ⟨“ ABCDEFG ”⟩ = 7
4 3 oveq2i ⊢ 0 ..^ ⟨“ ABCDEFG ”⟩ = 0 ..^ 7
5 4 feq2i ⊢ ⟨“ ABCDEFG ”⟩ : 0 ..^ ⟨“ ABCDEFG ”⟩ ⟶ V ↔ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ V
6 ffn ⊢ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ V → ⟨“ ABCDEFG ”⟩ Fn 0 ..^ 7
7 5 6 sylbi ⊢ ⟨“ ABCDEFG ”⟩ : 0 ..^ ⟨“ ABCDEFG ”⟩ ⟶ V → ⟨“ ABCDEFG ”⟩ Fn 0 ..^ 7
8 1 2 7 mp2b ⊢ ⟨“ ABCDEFG ”⟩ Fn 0 ..^ 7
9 8 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → ⟨“ ABCDEFG ”⟩ Fn 0 ..^ 7
10 dffn4 ⊢ ⟨“ ABCDEFG ”⟩ Fn 0 ..^ 7 ↔ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto ran ⁡ ⟨“ ABCDEFG ”⟩
11 9 10 sylib ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto ran ⁡ ⟨“ ABCDEFG ”⟩
12 simp1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V
13 12 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → A ∈ V
14 simp2 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → B ∈ V
15 14 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → B ∈ V
16 simp3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
17 16 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → C ∈ V
18 simp2 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → D ∈ V
19 simp1 ⊢ E ∈ V ∧ F ∈ V ∧ G ∈ V → E ∈ V
20 19 3ad2ant3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → E ∈ V
21 simp2 ⊢ E ∈ V ∧ F ∈ V ∧ G ∈ V → F ∈ V
22 21 3ad2ant3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → F ∈ V
23 simp3 ⊢ E ∈ V ∧ F ∈ V ∧ G ∈ V → G ∈ V
24 23 3ad2ant3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → G ∈ V
25 13 15 17 18 20 22 24 s7rn ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → ran ⁡ ⟨“ ABCDEFG ”⟩ = A B C ∪ D ∪ E F G
26 foeq3 ⊢ ran ⁡ ⟨“ ABCDEFG ”⟩ = A B C ∪ D ∪ E F G → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto ran ⁡ ⟨“ ABCDEFG ”⟩ ↔ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto A B C ∪ D ∪ E F G
27 25 26 syl ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto ran ⁡ ⟨“ ABCDEFG ”⟩ ↔ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto A B C ∪ D ∪ E F G
28 11 27 mpbid ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto A B C ∪ D ∪ E F G
29 28 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto A B C ∪ D ∪ E F G
30 7nn0 ⊢ 7 ∈ ℕ 0
31 hashfzo0 ⊢ 7 ∈ ℕ 0 → 0 ..^ 7 = 7
32 30 31 ax-mp ⊢ 0 ..^ 7 = 7
33 hash7g ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → A B C ∪ D ∪ E F G = 7
34 32 33 eqtr4id ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → 0 ..^ 7 = A B C ∪ D ∪ E F G
35 fzofi ⊢ 0 ..^ 7 ∈ Fin
36 tpfi ⊢ A B C ∈ Fin
37 snfi ⊢ D ∈ Fin
38 unfi ⊢ A B C ∈ Fin ∧ D ∈ Fin → A B C ∪ D ∈ Fin
39 36 37 38 mp2an ⊢ A B C ∪ D ∈ Fin
40 tpfi ⊢ E F G ∈ Fin
41 unfi ⊢ A B C ∪ D ∈ Fin ∧ E F G ∈ Fin → A B C ∪ D ∪ E F G ∈ Fin
42 39 40 41 mp2an ⊢ A B C ∪ D ∪ E F G ∈ Fin
43 hashen ⊢ 0 ..^ 7 ∈ Fin ∧ A B C ∪ D ∪ E F G ∈ Fin → 0 ..^ 7 = A B C ∪ D ∪ E F G ↔ 0 ..^ 7 ≈ A B C ∪ D ∪ E F G
44 35 42 43 mp2an ⊢ 0 ..^ 7 = A B C ∪ D ∪ E F G ↔ 0 ..^ 7 ≈ A B C ∪ D ∪ E F G
45 34 44 sylib ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → 0 ..^ 7 ≈ A B C ∪ D ∪ E F G
46 42 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → A B C ∪ D ∪ E F G ∈ Fin
47 fofinf1o ⊢ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ onto A B C ∪ D ∪ E F G ∧ 0 ..^ 7 ≈ A B C ∪ D ∪ E F G ∧ A B C ∪ D ∪ E F G ∈ Fin → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ 1-1 onto A B C ∪ D ∪ E F G
48 29 45 46 47 syl3anc ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ 1-1 onto A B C ∪ D ∪ E F G
49 f1oeq1 ⊢ K = ⟨“ ABCDEFG ”⟩ → K : 0 ..^ 7 ⟶ 1-1 onto A B C ∪ D ∪ E F G ↔ ⟨“ ABCDEFG ”⟩ : 0 ..^ 7 ⟶ 1-1 onto A B C ∪ D ∪ E F G
50 48 49 syl5ibrcom ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V ∧ G ∈ V ∧ A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E ∧ A ≠ F ∧ A ≠ G ∧ B ≠ C ∧ B ≠ D ∧ B ≠ E ∧ B ≠ F ∧ B ≠ G ∧ C ≠ D ∧ C ≠ E ∧ C ≠ F ∧ C ≠ G ∧ D ≠ E ∧ D ≠ F ∧ D ≠ G ∧ E ≠ F ∧ E ≠ G ∧ F ≠ G → K = ⟨“ ABCDEFG ”⟩ → K : 0 ..^ 7 ⟶ 1-1 onto A B C ∪ D ∪ E F G