This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3pthdlem1

Description: Lemma 1 for 3pthd . (Contributed by AV, 9-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
3wlkd.n ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) )
Assertion 3pthdlem1 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
2 3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3 3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
4 3wlkd.n ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) )
5 1 2 3 3wlkdlem3 ⊢ ( 𝜑 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) )
6 simpr1l ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → 𝐴 ≠ 𝐵 )
7 simpl ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
8 7 adantr ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( 𝑃 ‘ 0 ) = 𝐴 )
9 simpr ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( 𝑃 ‘ 1 ) = 𝐵 )
10 9 adantr ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( 𝑃 ‘ 1 ) = 𝐵 )
11 8 10 neeq12d ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ↔ 𝐴 ≠ 𝐵 ) )
12 11 adantr ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ↔ 𝐴 ≠ 𝐵 ) )
13 6 12 mpbird ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
14 13 a1d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
15 simpr1r ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → 𝐴 ≠ 𝐶 )
16 simpl ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( 𝑃 ‘ 2 ) = 𝐶 )
17 16 adantl ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( 𝑃 ‘ 2 ) = 𝐶 )
18 8 17 neeq12d ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐴 ≠ 𝐶 ) )
19 18 adantr ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐴 ≠ 𝐶 ) )
20 15 19 mpbird ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) )
21 20 a1d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
22 14 21 jca ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
23 eqid ⊢ 1 = 1
24 23 2a1i ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 1 ) = ( 𝑃 ‘ 1 ) → 1 = 1 ) )
25 24 necon3d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) )
26 simpr2l ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → 𝐵 ≠ 𝐶 )
27 10 17 neeq12d ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐵 ≠ 𝐶 ) )
28 27 adantr ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐵 ≠ 𝐶 ) )
29 26 28 mpbird ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) )
30 29 a1d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
31 25 30 jca ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
32 29 necomd ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) )
33 32 a1d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) )
34 eqid ⊢ 2 = 2
35 34 2a1i ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ 2 ) → 2 = 2 ) )
36 35 necon3d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) )
37 simpr2r ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → 𝐵 ≠ 𝐷 )
38 simpr ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( 𝑃 ‘ 3 ) = 𝐷 )
39 38 adantl ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( 𝑃 ‘ 3 ) = 𝐷 )
40 10 39 neeq12d ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ↔ 𝐵 ≠ 𝐷 ) )
41 40 adantr ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ↔ 𝐵 ≠ 𝐷 ) )
42 37 41 mpbird ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) )
43 42 necomd ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) )
44 43 a1d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) )
45 simp3 ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ≠ 𝐷 )
46 45 necomd ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) → 𝐷 ≠ 𝐶 )
47 46 adantl ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → 𝐷 ≠ 𝐶 )
48 simpl ⊢ ( ( ( 𝑃 ‘ 3 ) = 𝐷 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 3 ) = 𝐷 )
49 simpr ⊢ ( ( ( 𝑃 ‘ 3 ) = 𝐷 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 2 ) = 𝐶 )
50 48 49 neeq12d ⊢ ( ( ( 𝑃 ‘ 3 ) = 𝐷 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐷 ≠ 𝐶 ) )
51 50 ancoms ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐷 ≠ 𝐶 ) )
52 51 adantl ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐷 ≠ 𝐶 ) )
53 52 adantr ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐷 ≠ 𝐶 ) )
54 47 53 mpbird ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) )
55 54 a1d ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) )
56 44 55 jca ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
57 33 36 56 jca31 ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
58 22 31 57 jca31 ⊢ ( ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ∧ ( ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ) )
59 5 4 58 syl2anc ⊢ ( 𝜑 → ( ( ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ∧ ( ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ) )
60 1 fveq2i ⊢ ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ )
61 s4len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = 4
62 60 61 eqtri ⊢ ( ♯ ‘ 𝑃 ) = 4
63 62 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ 4 )
64 fzo0to42pr ⊢ ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } )
65 63 64 eqtri ⊢ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( { 0 , 1 } ∪ { 2 , 3 } )
66 65 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
67 ralunb ⊢ ( ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ∀ 𝑘 ∈ { 0 , 1 } ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ∀ 𝑘 ∈ { 2 , 3 } ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
68 c0ex ⊢ 0 ∈ V
69 1ex ⊢ 1 ∈ V
70 neeq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ≠ 1 ↔ 0 ≠ 1 ) )
71 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
72 71 neeq1d ⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
73 70 72 imbi12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ↔ ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
74 neeq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ≠ 2 ↔ 0 ≠ 2 ) )
75 71 neeq1d ⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
76 74 75 imbi12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ↔ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
77 73 76 anbi12d ⊢ ( 𝑘 = 0 → ( ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
78 neeq1 ⊢ ( 𝑘 = 1 → ( 𝑘 ≠ 1 ↔ 1 ≠ 1 ) )
79 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
80 79 neeq1d ⊢ ( 𝑘 = 1 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) )
81 78 80 imbi12d ⊢ ( 𝑘 = 1 → ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ↔ ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
82 neeq1 ⊢ ( 𝑘 = 1 → ( 𝑘 ≠ 2 ↔ 1 ≠ 2 ) )
83 79 neeq1d ⊢ ( 𝑘 = 1 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
84 82 83 imbi12d ⊢ ( 𝑘 = 1 → ( ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ↔ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
85 81 84 anbi12d ⊢ ( 𝑘 = 1 → ( ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
86 68 69 77 85 ralpr ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
87 2ex ⊢ 2 ∈ V
88 3ex ⊢ 3 ∈ V
89 neeq1 ⊢ ( 𝑘 = 2 → ( 𝑘 ≠ 1 ↔ 2 ≠ 1 ) )
90 fveq2 ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 2 ) )
91 90 neeq1d ⊢ ( 𝑘 = 2 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) )
92 89 91 imbi12d ⊢ ( 𝑘 = 2 → ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ↔ ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
93 neeq1 ⊢ ( 𝑘 = 2 → ( 𝑘 ≠ 2 ↔ 2 ≠ 2 ) )
94 90 neeq1d ⊢ ( 𝑘 = 2 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) )
95 93 94 imbi12d ⊢ ( 𝑘 = 2 → ( ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ↔ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
96 92 95 anbi12d ⊢ ( 𝑘 = 2 → ( ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
97 neeq1 ⊢ ( 𝑘 = 3 → ( 𝑘 ≠ 1 ↔ 3 ≠ 1 ) )
98 fveq2 ⊢ ( 𝑘 = 3 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 3 ) )
99 98 neeq1d ⊢ ( 𝑘 = 3 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) )
100 97 99 imbi12d ⊢ ( 𝑘 = 3 → ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ↔ ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
101 neeq1 ⊢ ( 𝑘 = 3 → ( 𝑘 ≠ 2 ↔ 3 ≠ 2 ) )
102 98 neeq1d ⊢ ( 𝑘 = 3 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) )
103 101 102 imbi12d ⊢ ( 𝑘 = 3 → ( ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ↔ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
104 100 103 anbi12d ⊢ ( 𝑘 = 3 → ( ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
105 87 88 96 104 ralpr ⊢ ( ∀ 𝑘 ∈ { 2 , 3 } ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
106 86 105 anbi12i ⊢ ( ( ∀ 𝑘 ∈ { 0 , 1 } ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ∀ 𝑘 ∈ { 2 , 3 } ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ↔ ( ( ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ∧ ( ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ) )
107 66 67 106 3bitri ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) ↔ ( ( ( ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 0 ≠ 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 1 ≠ 1 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 1 ≠ 2 → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ∧ ( ( ( 2 ≠ 1 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 2 ≠ 2 → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 2 ) ) ) ∧ ( ( 3 ≠ 1 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 3 ≠ 2 → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ) )
108 59 107 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
109 2 fveq2i ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 𝐾 𝐿 ”⟩ )
110 s3len ⊢ ( ♯ ‘ ⟨“ 𝐽 𝐾 𝐿 ”⟩ ) = 3
111 109 110 eqtri ⊢ ( ♯ ‘ 𝐹 ) = 3
112 111 oveq2i ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ..^ 3 )
113 fzo13pr ⊢ ( 1 ..^ 3 ) = { 1 , 2 }
114 112 113 eqtri ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = { 1 , 2 }
115 114 raleqi ⊢ ( ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ { 1 , 2 } ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
116 neeq2 ⊢ ( 𝑗 = 1 → ( 𝑘 ≠ 𝑗 ↔ 𝑘 ≠ 1 ) )
117 fveq2 ⊢ ( 𝑗 = 1 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 1 ) )
118 117 neeq2d ⊢ ( 𝑗 = 1 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) )
119 116 118 imbi12d ⊢ ( 𝑗 = 1 → ( ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
120 neeq2 ⊢ ( 𝑗 = 2 → ( 𝑘 ≠ 𝑗 ↔ 𝑘 ≠ 2 ) )
121 fveq2 ⊢ ( 𝑗 = 2 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 2 ) )
122 121 neeq2d ⊢ ( 𝑗 = 2 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) )
123 120 122 imbi12d ⊢ ( 𝑗 = 2 → ( ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
124 69 87 119 123 ralpr ⊢ ( ∀ 𝑗 ∈ { 1 , 2 } ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
125 115 124 bitri ⊢ ( ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
126 125 ralbii ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ( ( 𝑘 ≠ 1 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 1 ) ) ∧ ( 𝑘 ≠ 2 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
127 108 126 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑘 ≠ 𝑗 → ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )