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

Metamath Proof Explorer

Theorem sticksstones3

Proof