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 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑘𝑗 → ( 𝑃𝑘 ) ≠ ( 𝑃𝑗 ) ) )