sticksstones3

Description: The range function on strictly monotone functions with finite domain and codomain is an surjective mapping onto K -elemental sets. (Contributed by metakunt, 28-Sep-2024)

	Ref	Expression
Hypotheses	sticksstones3.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones3.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones3.3	$⊢ B = \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
	sticksstones3.4	$⊢ A = \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
	sticksstones3.5	$⊢ F = (z \in A ⟼ ran z)$
Assertion	sticksstones3	$⊢ φ \to F : A \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		sticksstones3.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones3.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones3.3	$⊢ B = \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
4		sticksstones3.4	$⊢ A = \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
5		sticksstones3.5	$⊢ F = (z \in A ⟼ ran z)$
6	1 2 3 4 5	sticksstones2	$⊢ φ \to F : A \underset{1-1}{⟶} B$
7		df-f1	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land Fun F^{-1})$
8	7	biimpi	$⊢ F : A \underset{1-1}{⟶} B \to (F : A ⟶ B \land Fun F^{-1})$
9	8	simpld	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
10	6 9	syl	$⊢ φ \to F : A ⟶ B$
11	3	eleq2i	$⊢ w \in B \leftrightarrow w \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
12	11	biimpi	$⊢ w \in B \to w \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
13	12	adantl	$⊢ (φ \land w \in B) \to w \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
14		fveqeq2	$⊢ a = w \to (\|a\| = K \leftrightarrow \|w\| = K)$
15	14	elrab	$⊢ w \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\} \leftrightarrow (w \in 𝒫 (1 \dots N) \land \|w\| = K)$
16	13 15	sylib	$⊢ (φ \land w \in B) \to (w \in 𝒫 (1 \dots N) \land \|w\| = K)$
17	16	simpld	$⊢ (φ \land w \in B) \to w \in 𝒫 (1 \dots N)$
18	17	elpwid	$⊢ (φ \land w \in B) \to w \subseteq (1 \dots N)$
19	18	sseld	$⊢ (φ \land w \in B) \to (c \in w \to c \in (1 \dots N))$
20	19	imp	$⊢ ((φ \land w \in B) \land c \in w) \to c \in (1 \dots N)$
21	20	3impa	$⊢ (φ \land w \in B \land c \in w) \to c \in (1 \dots N)$
22		elfznn	$⊢ c \in (1 \dots N) \to c \in ℕ$
23	21 22	syl	$⊢ (φ \land w \in B \land c \in w) \to c \in ℕ$
24	23	nnred	$⊢ (φ \land w \in B \land c \in w) \to c \in ℝ$
25	24	3expa	$⊢ ((φ \land w \in B) \land c \in w) \to c \in ℝ$
26	25	ex	$⊢ (φ \land w \in B) \to (c \in w \to c \in ℝ)$
27	26	ssrdv	$⊢ (φ \land w \in B) \to w \subseteq ℝ$
28		ltso	$⊢ < Or ℝ$
29		soss	$⊢ w \subseteq ℝ \to (< Or ℝ \to < Or w)$
30	28 29	mpi	$⊢ w \subseteq ℝ \to < Or w$
31	27 30	syl	$⊢ (φ \land w \in B) \to < Or w$
32		fzfid	$⊢ (φ \land w \in B) \to (1 \dots N) \in Fin$
33	32 18	ssfid	$⊢ (φ \land w \in B) \to w \in Fin$
34		fz1iso	$⊢ (< Or w \land w \in Fin) \to \exists v v {Isom}_{<, <} ((1 \dots \|w\|), w)$
35	31 33 34	syl2anc	$⊢ (φ \land w \in B) \to \exists v v {Isom}_{<, <} ((1 \dots \|w\|), w)$
36		df-isom	$⊢ v {Isom}_{<, <} ((1 \dots \|w\|), w) \leftrightarrow (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \land \forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \leftrightarrow v (x) < v (y)))$
37	36	biimpi	$⊢ v {Isom}_{<, <} ((1 \dots \|w\|), w) \to (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \land \forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \leftrightarrow v (x) < v (y)))$
38	37	3ad2ant3	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \land \forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \leftrightarrow v (x) < v (y)))$
39	38	simpld	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w$
40	16	simprd	$⊢ (φ \land w \in B) \to \|w\| = K$
41		oveq2	$⊢ \|w\| = K \to (1 \dots \|w\|) = (1 \dots K)$
42	41	f1oeq2d	$⊢ \|w\| = K \to (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \leftrightarrow v : (1 \dots K) \underset{1-1 onto}{⟶} w)$
43	40 42	syl	$⊢ (φ \land w \in B) \to (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \leftrightarrow v : (1 \dots K) \underset{1-1 onto}{⟶} w)$
44	43	biimpd	$⊢ (φ \land w \in B) \to (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \to v : (1 \dots K) \underset{1-1 onto}{⟶} w)$
45	44	3adant3	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (v : (1 \dots \|w\|) \underset{1-1 onto}{⟶} w \to v : (1 \dots K) \underset{1-1 onto}{⟶} w)$
46	39 45	mpd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v : (1 \dots K) \underset{1-1 onto}{⟶} w$
47		f1of	$⊢ v : (1 \dots K) \underset{1-1 onto}{⟶} w \to v : (1 \dots K) ⟶ w$
48	46 47	syl	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v : (1 \dots K) ⟶ w$
49	48	ffnd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v Fn (1 \dots K)$
50		ovexd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (1 \dots K) \in V$
51	49 50	fnexd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v \in V$
52	18	3adant3	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to w \subseteq (1 \dots N)$
53		fss	$⊢ (v : (1 \dots K) ⟶ w \land w \subseteq (1 \dots N)) \to v : (1 \dots K) ⟶ (1 \dots N)$
54	48 52 53	syl2anc	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v : (1 \dots K) ⟶ (1 \dots N)$
55	38	simprd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to \forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \leftrightarrow v (x) < v (y))$
56		biimp	$⊢ (x < y \leftrightarrow v (x) < v (y)) \to (x < y \to v (x) < v (y))$
57	56	a1i	$⊢ (((φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \land x \in (1 \dots \|w\|)) \land y \in (1 \dots \|w\|)) \to ((x < y \leftrightarrow v (x) < v (y)) \to (x < y \to v (x) < v (y)))$
58	57	ralimdva	$⊢ ((φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \land x \in (1 \dots \|w\|)) \to (\forall y \in (1 \dots \|w\|) (x < y \leftrightarrow v (x) < v (y)) \to \forall y \in (1 \dots \|w\|) (x < y \to v (x) < v (y)))$
59	58	ralimdva	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (\forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \leftrightarrow v (x) < v (y)) \to \forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \to v (x) < v (y)))$
60	55 59	mpd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to \forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \to v (x) < v (y))$
61	40	adantr	$⊢ ((φ \land w \in B) \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to \|w\| = K$
62	61	3impa	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to \|w\| = K$
63	62	oveq2d	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (1 \dots \|w\|) = (1 \dots K)$
64	63	raleqdv	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (\forall y \in (1 \dots \|w\|) (x < y \to v (x) < v (y)) \leftrightarrow \forall y \in (1 \dots K) (x < y \to v (x) < v (y)))$
65	64	adantr	$⊢ ((φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \land x \in (1 \dots \|w\|)) \to (\forall y \in (1 \dots \|w\|) (x < y \to v (x) < v (y)) \leftrightarrow \forall y \in (1 \dots K) (x < y \to v (x) < v (y)))$
66	63 65	raleqbidva	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (\forall x \in (1 \dots \|w\|) \forall y \in (1 \dots \|w\|) (x < y \to v (x) < v (y)) \leftrightarrow \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to v (x) < v (y)))$
67	60 66	mpbid	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to v (x) < v (y))$
68	54 67	jca	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (v : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to v (x) < v (y)))$
69		feq1	$⊢ f = v \to (f : (1 \dots K) ⟶ (1 \dots N) \leftrightarrow v : (1 \dots K) ⟶ (1 \dots N))$
70		fveq1	$⊢ f = v \to f (x) = v (x)$
71		fveq1	$⊢ f = v \to f (y) = v (y)$
72	70 71	breq12d	$⊢ f = v \to (f (x) < f (y) \leftrightarrow v (x) < v (y))$
73	72	imbi2d	$⊢ f = v \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to v (x) < v (y)))$
74	73	2ralbidv	$⊢ f = v \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)) \leftrightarrow \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to v (x) < v (y)))$
75	69 74	anbi12d	$⊢ f = v \to ((f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \leftrightarrow (v : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to v (x) < v (y))))$
76	51 68 75	elabd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
77	4	eleq2i	$⊢ v \in A \leftrightarrow v \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
78	76 77	sylibr	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to v \in A$
79	5	a1i	$⊢ (φ \land v \in A) \to F = (z \in A ⟼ ran z)$
80		simpr	$⊢ ((φ \land v \in A) \land z = v) \to z = v$
81	80	rneqd	$⊢ ((φ \land v \in A) \land z = v) \to ran z = ran v$
82		simpr	$⊢ (φ \land v \in A) \to v \in A$
83		rnexg	$⊢ v \in A \to ran v \in V$
84	82 83	syl	$⊢ (φ \land v \in A) \to ran v \in V$
85	79 81 82 84	fvmptd	$⊢ (φ \land v \in A) \to F (v) = ran v$
86	85	ex	$⊢ φ \to (v \in A \to F (v) = ran v)$
87	86	3ad2ant1	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (v \in A \to F (v) = ran v)$
88	78 87	mpd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to F (v) = ran v$
89		dff1o2	$⊢ v : (1 \dots K) \underset{1-1 onto}{⟶} w \leftrightarrow (v Fn (1 \dots K) \land Fun v^{-1} \land ran v = w)$
90	89	biimpi	$⊢ v : (1 \dots K) \underset{1-1 onto}{⟶} w \to (v Fn (1 \dots K) \land Fun v^{-1} \land ran v = w)$
91	90	simp3d	$⊢ v : (1 \dots K) \underset{1-1 onto}{⟶} w \to ran v = w$
92	46 91	syl	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to ran v = w$
93	88 92	eqtrd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to F (v) = w$
94	93	eqcomd	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to w = F (v)$
95	78 94	jca	$⊢ (φ \land w \in B \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (v \in A \land w = F (v))$
96	95	3expa	$⊢ ((φ \land w \in B) \land v {Isom}_{<, <} ((1 \dots \|w\|), w)) \to (v \in A \land w = F (v))$
97	96	ex	$⊢ (φ \land w \in B) \to (v {Isom}_{<, <} ((1 \dots \|w\|), w) \to (v \in A \land w = F (v)))$
98	97	eximdv	$⊢ (φ \land w \in B) \to (\exists v v {Isom}_{<, <} ((1 \dots \|w\|), w) \to \exists v (v \in A \land w = F (v)))$
99	35 98	mpd	$⊢ (φ \land w \in B) \to \exists v (v \in A \land w = F (v))$
100		df-rex	$⊢ \exists v \in A w = F (v) \leftrightarrow \exists v (v \in A \land w = F (v))$
101	99 100	sylibr	$⊢ (φ \land w \in B) \to \exists v \in A w = F (v)$
102	101	ralrimiva	$⊢ φ \to \forall w \in B \exists v \in A w = F (v)$
103	10 102	jca	$⊢ φ \to (F : A ⟶ B \land \forall w \in B \exists v \in A w = F (v))$
104		dffo3	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall w \in B \exists v \in A w = F (v))$
105	104	a1i	$⊢ φ \to (F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall w \in B \exists v \in A w = F (v)))$
106	103 105	mpbird	$⊢ φ \to F : A \underset{onto}{⟶} B$

Metamath Proof Explorer

Theorem sticksstones3

Proof