Metamath Proof Explorer

Theorem s3f1

Description: Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses s3f1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
s3f1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
s3f1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
s3f1.1 ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
s3f1.2 ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
s3f1.3 ⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
Assertion s3f1 ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 )

Proof

Step Hyp Ref Expression
1 s3f1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
2 s3f1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
3 s3f1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
4 s3f1.1 ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
5 s3f1.2 ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
6 s3f1.3 ⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
7 1 2 3 s3cld ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 )
8 wrdf ⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) ⟶ 𝐷 )
9 7 8 syl ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) ⟶ 𝐷 )
10 9 ffdmd ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ⟶ 𝐷 )
11 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 0 ) → 𝑖 = 0 )
12 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 0 ) → 𝑗 = 0 )
13 11 12 eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 0 ) → 𝑖 = 𝑗 )
14 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) )
15 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) → 𝑖 = 0 )
16 15 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) )
17 s3fv0 ⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
18 1 17 syl ⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
19 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
20 16 19 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐼 )
21 20 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐼 )
22 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 1 ) → 𝑗 = 1 )
23 22 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) )
24 s3fv1 ⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
25 2 24 syl ⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
26 25 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
27 23 26 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐽 )
28 27 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐽 )
29 14 21 28 3eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 1 ) → 𝐼 = 𝐽 )
30 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 1 ) → 𝐼 ≠ 𝐽 )
31 29 30 pm2.21ddne ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 1 ) → 𝑖 = 𝑗 )
32 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) )
33 20 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐼 )
34 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 2 ) → 𝑗 = 2 )
35 34 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) )
36 s3fv2 ⊢ ( 𝐾 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
37 3 36 syl ⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
38 37 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
39 35 38 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐾 )
40 39 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐾 )
41 32 33 40 3eqtr3rd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 2 ) → 𝐾 = 𝐼 )
42 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 2 ) → 𝐾 ≠ 𝐼 )
43 41 42 pm2.21ddne ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) ∧ 𝑗 = 2 ) → 𝑖 = 𝑗 )
44 wrddm ⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 → dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ = ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) )
45 7 44 syl ⊢ ( 𝜑 → dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ = ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) )
46 s3len ⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3
47 46 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) = ( 0 ..^ 3 )
48 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
49 47 48 eqtri ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) = { 0 , 1 , 2 }
50 45 49 eqtrdi ⊢ ( 𝜑 → dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ = { 0 , 1 , 2 } )
51 50 eleq2d ⊢ ( 𝜑 → ( 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ↔ 𝑗 ∈ { 0 , 1 , 2 } ) )
52 51 biimpa ⊢ ( ( 𝜑 ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) → 𝑗 ∈ { 0 , 1 , 2 } )
53 vex ⊢ 𝑗 ∈ V
54 53 eltp ⊢ ( 𝑗 ∈ { 0 , 1 , 2 } ↔ ( 𝑗 = 0 ∨ 𝑗 = 1 ∨ 𝑗 = 2 ) )
55 52 54 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) → ( 𝑗 = 0 ∨ 𝑗 = 1 ∨ 𝑗 = 2 ) )
56 55 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) → ( 𝑗 = 0 ∨ 𝑗 = 1 ∨ 𝑗 = 2 ) )
57 56 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) → ( 𝑗 = 0 ∨ 𝑗 = 1 ∨ 𝑗 = 2 ) )
58 13 31 43 57 mpjao3dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 0 ) → 𝑖 = 𝑗 )
59 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) )
60 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) → 𝑖 = 1 )
61 60 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) )
62 25 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
63 61 62 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐽 )
64 63 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐽 )
65 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 0 ) → 𝑗 = 0 )
66 65 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) )
67 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
68 66 67 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐼 )
69 68 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐼 )
70 59 64 69 3eqtr3rd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 0 ) → 𝐼 = 𝐽 )
71 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 0 ) → 𝐼 ≠ 𝐽 )
72 70 71 pm2.21ddne ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 0 ) → 𝑖 = 𝑗 )
73 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 1 ) → 𝑖 = 1 )
74 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 1 ) → 𝑗 = 1 )
75 73 74 eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 1 ) → 𝑖 = 𝑗 )
76 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) )
77 63 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐽 )
78 39 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐾 )
79 76 77 78 3eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 2 ) → 𝐽 = 𝐾 )
80 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 2 ) → 𝐽 ≠ 𝐾 )
81 79 80 pm2.21ddne ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) ∧ 𝑗 = 2 ) → 𝑖 = 𝑗 )
82 56 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) → ( 𝑗 = 0 ∨ 𝑗 = 1 ∨ 𝑗 = 2 ) )
83 72 75 81 82 mpjao3dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 1 ) → 𝑖 = 𝑗 )
84 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) )
85 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) → 𝑖 = 2 )
86 85 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) )
87 37 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
88 86 87 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐾 )
89 88 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐾 )
90 68 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 0 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐼 )
91 84 89 90 3eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 0 ) → 𝐾 = 𝐼 )
92 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 0 ) → 𝐾 ≠ 𝐼 )
93 91 92 pm2.21ddne ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 0 ) → 𝑖 = 𝑗 )
94 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) )
95 88 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = 𝐾 )
96 27 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 1 ) → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) = 𝐽 )
97 94 95 96 3eqtr3rd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 1 ) → 𝐽 = 𝐾 )
98 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 1 ) → 𝐽 ≠ 𝐾 )
99 97 98 pm2.21ddne ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 1 ) → 𝑖 = 𝑗 )
100 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 2 ) → 𝑖 = 2 )
101 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 2 ) → 𝑗 = 2 )
102 100 101 eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) ∧ 𝑗 = 2 ) → 𝑖 = 𝑗 )
103 56 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) → ( 𝑗 = 0 ∨ 𝑗 = 1 ∨ 𝑗 = 2 ) )
104 93 99 102 103 mpjao3dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) ∧ 𝑖 = 2 ) → 𝑖 = 𝑗 )
105 50 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ↔ 𝑖 ∈ { 0 , 1 , 2 } ) )
106 105 biimpa ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) → 𝑖 ∈ { 0 , 1 , 2 } )
107 vex ⊢ 𝑖 ∈ V
108 107 eltp ⊢ ( 𝑖 ∈ { 0 , 1 , 2 } ↔ ( 𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2 ) )
109 106 108 sylib ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) → ( 𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2 ) )
110 109 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) → ( 𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2 ) )
111 58 83 104 110 mpjao3dan ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) ) → 𝑖 = 𝑗 )
112 111 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) → ( ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
113 112 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∧ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) → ( ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
114 113 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ( ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
115 dff13 ⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 ↔ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ⟶ 𝐷 ∧ ∀ 𝑖 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∀ 𝑗 ∈ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ( ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑖 ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
116 10 114 115 sylanbrc ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 )