Metamath Proof Explorer


Theorem f1dom3el3dif

Description: The range of a 1-1 function from a set with three different elements has (at least) three different elements. (Contributed by AV, 20-Mar-2019)

Ref Expression
Hypotheses f1dom3fv3dif.v ( 𝜑 → ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) )
f1dom3fv3dif.n ( 𝜑 → ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) )
f1dom3fv3dif.f ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1𝑅 )
Assertion f1dom3el3dif ( 𝜑 → ∃ 𝑥𝑅𝑦𝑅𝑧𝑅 ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) )

Proof

Step Hyp Ref Expression
1 f1dom3fv3dif.v ( 𝜑 → ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) )
2 f1dom3fv3dif.n ( 𝜑 → ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) )
3 f1dom3fv3dif.f ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1𝑅 )
4 f1f ( 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1𝑅𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 )
5 simpr ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 )
6 eqidd ( 𝜑𝐴 = 𝐴 )
7 6 3mix1d ( 𝜑 → ( 𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶 ) )
8 1 simp1d ( 𝜑𝐴𝑋 )
9 eltpg ( 𝐴𝑋 → ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶 ) ) )
10 8 9 syl ( 𝜑 → ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶 ) ) )
11 7 10 mpbird ( 𝜑𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
12 11 adantr ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
13 5 12 ffvelrnd ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( 𝐹𝐴 ) ∈ 𝑅 )
14 eqidd ( 𝜑𝐵 = 𝐵 )
15 14 3mix2d ( 𝜑 → ( 𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶 ) )
16 1 simp2d ( 𝜑𝐵𝑌 )
17 eltpg ( 𝐵𝑌 → ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶 ) ) )
18 16 17 syl ( 𝜑 → ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶 ) ) )
19 15 18 mpbird ( 𝜑𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
20 19 adantr ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
21 5 20 ffvelrnd ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( 𝐹𝐵 ) ∈ 𝑅 )
22 1 simp3d ( 𝜑𝐶𝑍 )
23 tpid3g ( 𝐶𝑍𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
24 22 23 syl ( 𝜑𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
25 24 adantr ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
26 5 25 ffvelrnd ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( 𝐹𝐶 ) ∈ 𝑅 )
27 13 21 26 3jca ( ( 𝜑𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( ( 𝐹𝐴 ) ∈ 𝑅 ∧ ( 𝐹𝐵 ) ∈ 𝑅 ∧ ( 𝐹𝐶 ) ∈ 𝑅 ) )
28 27 expcom ( 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 → ( 𝜑 → ( ( 𝐹𝐴 ) ∈ 𝑅 ∧ ( 𝐹𝐵 ) ∈ 𝑅 ∧ ( 𝐹𝐶 ) ∈ 𝑅 ) ) )
29 4 28 syl ( 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1𝑅 → ( 𝜑 → ( ( 𝐹𝐴 ) ∈ 𝑅 ∧ ( 𝐹𝐵 ) ∈ 𝑅 ∧ ( 𝐹𝐶 ) ∈ 𝑅 ) ) )
30 3 29 mpcom ( 𝜑 → ( ( 𝐹𝐴 ) ∈ 𝑅 ∧ ( 𝐹𝐵 ) ∈ 𝑅 ∧ ( 𝐹𝐶 ) ∈ 𝑅 ) )
31 1 2 3 f1dom3fv3dif ( 𝜑 → ( ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ∧ ( 𝐹𝐴 ) ≠ ( 𝐹𝐶 ) ∧ ( 𝐹𝐵 ) ≠ ( 𝐹𝐶 ) ) )
32 neeq1 ( 𝑥 = ( 𝐹𝐴 ) → ( 𝑥𝑦 ↔ ( 𝐹𝐴 ) ≠ 𝑦 ) )
33 neeq1 ( 𝑥 = ( 𝐹𝐴 ) → ( 𝑥𝑧 ↔ ( 𝐹𝐴 ) ≠ 𝑧 ) )
34 32 33 3anbi12d ( 𝑥 = ( 𝐹𝐴 ) → ( ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) ↔ ( ( 𝐹𝐴 ) ≠ 𝑦 ∧ ( 𝐹𝐴 ) ≠ 𝑧𝑦𝑧 ) ) )
35 neeq2 ( 𝑦 = ( 𝐹𝐵 ) → ( ( 𝐹𝐴 ) ≠ 𝑦 ↔ ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ) )
36 neeq1 ( 𝑦 = ( 𝐹𝐵 ) → ( 𝑦𝑧 ↔ ( 𝐹𝐵 ) ≠ 𝑧 ) )
37 35 36 3anbi13d ( 𝑦 = ( 𝐹𝐵 ) → ( ( ( 𝐹𝐴 ) ≠ 𝑦 ∧ ( 𝐹𝐴 ) ≠ 𝑧𝑦𝑧 ) ↔ ( ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ∧ ( 𝐹𝐴 ) ≠ 𝑧 ∧ ( 𝐹𝐵 ) ≠ 𝑧 ) ) )
38 neeq2 ( 𝑧 = ( 𝐹𝐶 ) → ( ( 𝐹𝐴 ) ≠ 𝑧 ↔ ( 𝐹𝐴 ) ≠ ( 𝐹𝐶 ) ) )
39 neeq2 ( 𝑧 = ( 𝐹𝐶 ) → ( ( 𝐹𝐵 ) ≠ 𝑧 ↔ ( 𝐹𝐵 ) ≠ ( 𝐹𝐶 ) ) )
40 38 39 3anbi23d ( 𝑧 = ( 𝐹𝐶 ) → ( ( ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ∧ ( 𝐹𝐴 ) ≠ 𝑧 ∧ ( 𝐹𝐵 ) ≠ 𝑧 ) ↔ ( ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ∧ ( 𝐹𝐴 ) ≠ ( 𝐹𝐶 ) ∧ ( 𝐹𝐵 ) ≠ ( 𝐹𝐶 ) ) ) )
41 34 37 40 rspc3ev ( ( ( ( 𝐹𝐴 ) ∈ 𝑅 ∧ ( 𝐹𝐵 ) ∈ 𝑅 ∧ ( 𝐹𝐶 ) ∈ 𝑅 ) ∧ ( ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ∧ ( 𝐹𝐴 ) ≠ ( 𝐹𝐶 ) ∧ ( 𝐹𝐵 ) ≠ ( 𝐹𝐶 ) ) ) → ∃ 𝑥𝑅𝑦𝑅𝑧𝑅 ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) )
42 30 31 41 syl2anc ( 𝜑 → ∃ 𝑥𝑅𝑦𝑅𝑧𝑅 ( 𝑥𝑦𝑥𝑧𝑦𝑧 ) )