Metamath Proof Explorer

Theorem f1dom3el3dif

Description: The codomain 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 )
14 eqidd ⊢ ( 𝜑 → 𝐵 = 𝐵 )
15 14 3mix2d ⊢ ( 𝜑 → ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶 ) )
16 1 simp2d ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
17 eltpg ⊢ ( 𝐵 ∈ 𝑌 → ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶 ) ) )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶 ) ) )
19 15 18 mpbird ⊢ ( 𝜑 → 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
21 5 20 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝑅 )
22 1 simp3d ⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
23 tpid3g ⊢ ( 𝐶 ∈ 𝑍 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
24 22 23 syl ⊢ ( 𝜑 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
26 5 25 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐹 : { 𝐴 , 𝐵 , 𝐶 } ⟶ 𝑅 ) → ( 𝐹 ‘ 𝐶 ) ∈ 𝑅 )
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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 ∃ 𝑧 ∈ 𝑅 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) )