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 ⊢φ→A∈X∧B∈Y∧C∈Z
f1dom3fv3dif.n ⊢φ→A≠B∧A≠C∧B≠C
f1dom3fv3dif.f ⊢φ→F:ABC⟶1-1R
Assertion f1dom3el3dif ⊢φ→∃x∈R∃y∈R∃z∈Rx≠y∧x≠z∧y≠z

Proof

Step Hyp Ref Expression
1 f1dom3fv3dif.v ⊢φ→A∈X∧B∈Y∧C∈Z
2 f1dom3fv3dif.n ⊢φ→A≠B∧A≠C∧B≠C
3 f1dom3fv3dif.f ⊢φ→F:ABC⟶1-1R
4 f1f ⊢F:ABC⟶1-1R→F:ABC⟶R
5 simpr ⊢φ∧F:ABC⟶R→F:ABC⟶R
6 eqidd ⊢φ→A=A
7 6 3mix1d ⊢φ→A=A∨A=B∨A=C
8 1 simp1d ⊢φ→A∈X
9 eltpg ⊢A∈X→A∈ABC↔A=A∨A=B∨A=C
10 8 9 syl ⊢φ→A∈ABC↔A=A∨A=B∨A=C
11 7 10 mpbird ⊢φ→A∈ABC
12 11 adantr ⊢φ∧F:ABC⟶R→A∈ABC
13 5 12 ffvelcdmd ⊢φ∧F:ABC⟶R→F⁡A∈R
14 eqidd ⊢φ→B=B
15 14 3mix2d ⊢φ→B=A∨B=B∨B=C
16 1 simp2d ⊢φ→B∈Y
17 eltpg ⊢B∈Y→B∈ABC↔B=A∨B=B∨B=C
18 16 17 syl ⊢φ→B∈ABC↔B=A∨B=B∨B=C
19 15 18 mpbird ⊢φ→B∈ABC
20 19 adantr ⊢φ∧F:ABC⟶R→B∈ABC
21 5 20 ffvelcdmd ⊢φ∧F:ABC⟶R→F⁡B∈R
22 1 simp3d ⊢φ→C∈Z
23 tpid3g ⊢C∈Z→C∈ABC
24 22 23 syl ⊢φ→C∈ABC
25 24 adantr ⊢φ∧F:ABC⟶R→C∈ABC
26 5 25 ffvelcdmd ⊢φ∧F:ABC⟶R→F⁡C∈R
27 13 21 26 3jca ⊢φ∧F:ABC⟶R→F⁡A∈R∧F⁡B∈R∧F⁡C∈R
28 27 expcom ⊢F:ABC⟶R→φ→F⁡A∈R∧F⁡B∈R∧F⁡C∈R
29 4 28 syl ⊢F:ABC⟶1-1R→φ→F⁡A∈R∧F⁡B∈R∧F⁡C∈R
30 3 29 mpcom ⊢φ→F⁡A∈R∧F⁡B∈R∧F⁡C∈R
31 1 2 3 f1dom3fv3dif ⊢φ→F⁡A≠F⁡B∧F⁡A≠F⁡C∧F⁡B≠F⁡C
32 neeq1 ⊢x=F⁡A→x≠y↔F⁡A≠y
33 neeq1 ⊢x=F⁡A→x≠z↔F⁡A≠z
34 32 33 3anbi12d ⊢x=F⁡A→x≠y∧x≠z∧y≠z↔F⁡A≠y∧F⁡A≠z∧y≠z
35 neeq2 ⊢y=F⁡B→F⁡A≠y↔F⁡A≠F⁡B
36 neeq1 ⊢y=F⁡B→y≠z↔F⁡B≠z
37 35 36 3anbi13d ⊢y=F⁡B→F⁡A≠y∧F⁡A≠z∧y≠z↔F⁡A≠F⁡B∧F⁡A≠z∧F⁡B≠z
38 neeq2 ⊢z=F⁡C→F⁡A≠z↔F⁡A≠F⁡C
39 neeq2 ⊢z=F⁡C→F⁡B≠z↔F⁡B≠F⁡C
40 38 39 3anbi23d ⊢z=F⁡C→F⁡A≠F⁡B∧F⁡A≠z∧F⁡B≠z↔F⁡A≠F⁡B∧F⁡A≠F⁡C∧F⁡B≠F⁡C
41 34 37 40 rspc3ev ⊢F⁡A∈R∧F⁡B∈R∧F⁡C∈R∧F⁡A≠F⁡B∧F⁡A≠F⁡C∧F⁡B≠F⁡C→∃x∈R∃y∈R∃z∈Rx≠y∧x≠z∧y≠z
42 30 31 41 syl2anc ⊢φ→∃x∈R∃y∈R∃z∈Rx≠y∧x≠z∧y≠z