sticksstones2

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

	Ref	Expression
Hypotheses	sticksstones2.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones2.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones2.3	$⊢ B = \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
	sticksstones2.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)))\}$
	sticksstones2.5	$⊢ F = (z \in A ⟼ ran z)$
Assertion	sticksstones2	$⊢ φ \to F : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		sticksstones2.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones2.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones2.3	$⊢ B = \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
4		sticksstones2.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		sticksstones2.5	$⊢ F = (z \in A ⟼ ran z)$
6		fveqeq2	$⊢ a = ran z \to (\|a\| = K \leftrightarrow \|ran z\| = K)$
7		fzfid	$⊢ (φ \land z \in A) \to (1 \dots N) \in Fin$
8		eleq1w	$⊢ f = z \to (f \in A \leftrightarrow z \in A)$
9		feq1	$⊢ f = z \to (f : (1 \dots K) ⟶ (1 \dots N) \leftrightarrow z : (1 \dots K) ⟶ (1 \dots N))$
10		fveq1	$⊢ f = z \to f (x) = z (x)$
11		fveq1	$⊢ f = z \to f (y) = z (y)$
12	10 11	breq12d	$⊢ f = z \to (f (x) < f (y) \leftrightarrow z (x) < z (y))$
13	12	imbi2d	$⊢ f = z \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to z (x) < z (y)))$
14	13	ralbidv	$⊢ f = z \to (\forall y \in (1 \dots K) (x < y \to f (x) < f (y)) \leftrightarrow \forall y \in (1 \dots K) (x < y \to z (x) < z (y)))$
15	14	ralbidv	$⊢ f = z \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 z (x) < z (y)))$
16	9 15	anbi12d	$⊢ f = z \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 (z : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y))))$
17	8 16	bibi12d	$⊢ f = z \to ((f \in A \leftrightarrow (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 (z \in A \leftrightarrow (z : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)))))$
18		eqabb	$⊢ 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)))\} \leftrightarrow \forall f (f \in A \leftrightarrow (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))))$
19	4 18	mpbi	$⊢ \forall f (f \in A \leftrightarrow (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))))$
20	19	spi	$⊢ f \in A \leftrightarrow (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)))$
21	17 20	chvarvv	$⊢ z \in A \leftrightarrow (z : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)))$
22	21	bilani	$⊢ (φ \land z \in A) \to (z : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)))$
23	22	simpld	$⊢ (φ \land z \in A) \to z : (1 \dots K) ⟶ (1 \dots N)$
24	23	frnd	$⊢ (φ \land z \in A) \to ran z \subseteq (1 \dots N)$
25	7 24	sselpwd	$⊢ (φ \land z \in A) \to ran z \in 𝒫 (1 \dots N)$
26	23	ffnd	$⊢ (φ \land z \in A) \to z Fn (1 \dots K)$
27		hashfn	$⊢ z Fn (1 \dots K) \to \|z\| = \|(1 \dots K)\|$
28	26 27	syl	$⊢ (φ \land z \in A) \to \|z\| = \|(1 \dots K)\|$
29	2	adantr	$⊢ (φ \land z \in A) \to K \in ℕ_{0}$
30		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
31	29 30	syl	$⊢ (φ \land z \in A) \to \|(1 \dots K)\| = K$
32	28 31	eqtrd	$⊢ (φ \land z \in A) \to \|z\| = K$
33	32	eqcomd	$⊢ (φ \land z \in A) \to K = \|z\|$
34		fzfid	$⊢ (φ \land z \in A) \to (1 \dots K) \in Fin$
35		elfznn	$⊢ a \in (1 \dots K) \to a \in ℕ$
36	35	3ad2ant3	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to a \in ℕ$
37	36	nnred	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to a \in ℝ$
38	37	adantr	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to a \in ℝ$
39		elfznn	$⊢ b \in (1 \dots K) \to b \in ℕ$
40	39	nnred	$⊢ b \in (1 \dots K) \to b \in ℝ$
41	40	adantl	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to b \in ℝ$
42		lttri2	$⊢ (a \in ℝ \land b \in ℝ) \to (a \neq b \leftrightarrow (a < b \lor b < a))$
43	38 41 42	syl2anc	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (a \neq b \leftrightarrow (a < b \lor b < a))$
44	23	3adant3	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to z : (1 \dots K) ⟶ (1 \dots N)$
45		simp3	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to a \in (1 \dots K)$
46	44 45	ffvelcdmd	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to z (a) \in (1 \dots N)$
47	46	adantr	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to z (a) \in (1 \dots N)$
48	47	adantr	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land a < b) \to z (a) \in (1 \dots N)$
49		elfznn	$⊢ z (a) \in (1 \dots N) \to z (a) \in ℕ$
50	48 49	syl	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land a < b) \to z (a) \in ℕ$
51	50	nnred	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land a < b) \to z (a) \in ℝ$
52	22	simprd	$⊢ (φ \land z \in A) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y))$
53	52	3adant3	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y))$
54	53	adantr	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y))$
55	45	adantr	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to a \in (1 \dots K)$
56		simpr	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to b \in (1 \dots K)$
57		breq1	$⊢ x = a \to (x < y \leftrightarrow a < y)$
58		fveq2	$⊢ x = a \to z (x) = z (a)$
59	58	breq1d	$⊢ x = a \to (z (x) < z (y) \leftrightarrow z (a) < z (y))$
60	57 59	imbi12d	$⊢ x = a \to ((x < y \to z (x) < z (y)) \leftrightarrow (a < y \to z (a) < z (y)))$
61		breq2	$⊢ y = b \to (a < y \leftrightarrow a < b)$
62		fveq2	$⊢ y = b \to z (y) = z (b)$
63	62	breq2d	$⊢ y = b \to (z (a) < z (y) \leftrightarrow z (a) < z (b))$
64	61 63	imbi12d	$⊢ y = b \to ((a < y \to z (a) < z (y)) \leftrightarrow (a < b \to z (a) < z (b)))$
65	60 64	rspc2v	$⊢ (a \in (1 \dots K) \land b \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)) \to (a < b \to z (a) < z (b)))$
66	55 56 65	syl2anc	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)) \to (a < b \to z (a) < z (b)))$
67	54 66	mpd	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (a < b \to z (a) < z (b))$
68	67	imp	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land a < b) \to z (a) < z (b)$
69	51 68	ltned	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land a < b) \to z (a) \neq z (b)$
70	44	ffvelcdmda	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to z (b) \in (1 \dots N)$
71		elfznn	$⊢ z (b) \in (1 \dots N) \to z (b) \in ℕ$
72	70 71	syl	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to z (b) \in ℕ$
73	72	nnred	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to z (b) \in ℝ$
74	73	adantr	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land b < a) \to z (b) \in ℝ$
75		breq1	$⊢ x = b \to (x < y \leftrightarrow b < y)$
76		fveq2	$⊢ x = b \to z (x) = z (b)$
77	76	breq1d	$⊢ x = b \to (z (x) < z (y) \leftrightarrow z (b) < z (y))$
78	75 77	imbi12d	$⊢ x = b \to ((x < y \to z (x) < z (y)) \leftrightarrow (b < y \to z (b) < z (y)))$
79		breq2	$⊢ y = a \to (b < y \leftrightarrow b < a)$
80		fveq2	$⊢ y = a \to z (y) = z (a)$
81	80	breq2d	$⊢ y = a \to (z (b) < z (y) \leftrightarrow z (b) < z (a))$
82	79 81	imbi12d	$⊢ y = a \to ((b < y \to z (b) < z (y)) \leftrightarrow (b < a \to z (b) < z (a)))$
83	78 82	rspc2v	$⊢ (b \in (1 \dots K) \land a \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)) \to (b < a \to z (b) < z (a)))$
84	56 55 83	syl2anc	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to z (x) < z (y)) \to (b < a \to z (b) < z (a)))$
85	54 84	mpd	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (b < a \to z (b) < z (a))$
86	85	imp	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land b < a) \to z (b) < z (a)$
87	74 86	ltned	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land b < a) \to z (b) \neq z (a)$
88	87	necomd	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land b < a) \to z (a) \neq z (b)$
89	69 88	jaodan	$⊢ (((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \land (a < b \lor b < a)) \to z (a) \neq z (b)$
90	89	ex	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to ((a < b \lor b < a) \to z (a) \neq z (b))$
91	43 90	sylbid	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (a \neq b \to z (a) \neq z (b))$
92	91	necon4d	$⊢ ((φ \land z \in A \land a \in (1 \dots K)) \land b \in (1 \dots K)) \to (z (a) = z (b) \to a = b)$
93	92	ralrimiva	$⊢ (φ \land z \in A \land a \in (1 \dots K)) \to \forall b \in (1 \dots K) (z (a) = z (b) \to a = b)$
94	93	3expa	$⊢ ((φ \land z \in A) \land a \in (1 \dots K)) \to \forall b \in (1 \dots K) (z (a) = z (b) \to a = b)$
95	94	ralrimiva	$⊢ (φ \land z \in A) \to \forall a \in (1 \dots K) \forall b \in (1 \dots K) (z (a) = z (b) \to a = b)$
96	23 95	jca	$⊢ (φ \land z \in A) \to (z : (1 \dots K) ⟶ (1 \dots N) \land \forall a \in (1 \dots K) \forall b \in (1 \dots K) (z (a) = z (b) \to a = b))$
97		dff13	$⊢ z : (1 \dots K) \underset{1-1}{⟶} (1 \dots N) \leftrightarrow (z : (1 \dots K) ⟶ (1 \dots N) \land \forall a \in (1 \dots K) \forall b \in (1 \dots K) (z (a) = z (b) \to a = b))$
98	96 97	sylibr	$⊢ (φ \land z \in A) \to z : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)$
99		hashf1rn	$⊢ ((1 \dots K) \in Fin \land z : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)) \to \|z\| = \|ran z\|$
100	34 98 99	syl2anc	$⊢ (φ \land z \in A) \to \|z\| = \|ran z\|$
101	33 100	eqtrd	$⊢ (φ \land z \in A) \to K = \|ran z\|$
102	101	eqcomd	$⊢ (φ \land z \in A) \to \|ran z\| = K$
103	6 25 102	elrabd	$⊢ (φ \land z \in A) \to ran z \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
104	3	eleq2i	$⊢ ran z \in B \leftrightarrow ran z \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
105	104	a1i	$⊢ (φ \land z \in A) \to (ran z \in B \leftrightarrow ran z \in \{a \in 𝒫 (1 \dots N) \| \|a\| = K\})$
106	103 105	mpbird	$⊢ (φ \land z \in A) \to ran z \in B$
107	106 5	fmptd	$⊢ φ \to F : A ⟶ B$
108	1	3ad2ant1	$⊢ (φ \land i \in A \land j \in A) \to N \in ℕ_{0}$
109	108	adantr	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to N \in ℕ_{0}$
110	2	3ad2ant1	$⊢ (φ \land i \in A \land j \in A) \to K \in ℕ_{0}$
111	110	adantr	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to K \in ℕ_{0}$
112		simpl2	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to i \in A$
113		simpl3	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to j \in A$
114		simpr	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to i \neq j$
115		fveq2	$⊢ r = s \to i (r) = i (s)$
116		fveq2	$⊢ r = s \to j (r) = j (s)$
117	115 116	neeq12d	$⊢ r = s \to (i (r) \neq j (r) \leftrightarrow i (s) \neq j (s))$
118	117	cbvrabv	$⊢ \{r \in (1 \dots K) \| i (r) \neq j (r)\} = \{s \in (1 \dots K) \| i (s) \neq j (s)\}$
119	118	infeq1i	$⊢ inf (\{r \in (1 \dots K) \| i (r) \neq j (r)\} ℝ <) = inf (\{s \in (1 \dots K) \| i (s) \neq j (s)\} ℝ <)$
120	109 111 4 112 113 114 119	sticksstones1	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to ran i \neq ran j$
121	5	a1i	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to F = (z \in A ⟼ ran z)$
122		simpr	$⊢ (((φ \land i \in A \land j \in A) \land i \neq j) \land z = i) \to z = i$
123	122	rneqd	$⊢ (((φ \land i \in A \land j \in A) \land i \neq j) \land z = i) \to ran z = ran i$
124		fzfid	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to (1 \dots N) \in Fin$
125		eleq1w	$⊢ f = i \to (f \in A \leftrightarrow i \in A)$
126		feq1	$⊢ f = i \to (f : (1 \dots K) ⟶ (1 \dots N) \leftrightarrow i : (1 \dots K) ⟶ (1 \dots N))$
127		fveq1	$⊢ f = i \to f (x) = i (x)$
128		fveq1	$⊢ f = i \to f (y) = i (y)$
129	127 128	breq12d	$⊢ f = i \to (f (x) < f (y) \leftrightarrow i (x) < i (y))$
130	129	imbi2d	$⊢ f = i \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to i (x) < i (y)))$
131	130	2ralbidv	$⊢ f = i \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 i (x) < i (y)))$
132	126 131	anbi12d	$⊢ f = i \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 (i : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to i (x) < i (y))))$
133	125 132	bibi12d	$⊢ f = i \to ((f \in A \leftrightarrow (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 (i \in A \leftrightarrow (i : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to i (x) < i (y)))))$
134	133 20	chvarvv	$⊢ i \in A \leftrightarrow (i : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to i (x) < i (y)))$
135	134	bilani	$⊢ (φ \land i \in A) \to (i : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to i (x) < i (y)))$
136	135	simpld	$⊢ (φ \land i \in A) \to i : (1 \dots K) ⟶ (1 \dots N)$
137	136	3adant3	$⊢ (φ \land i \in A \land j \in A) \to i : (1 \dots K) ⟶ (1 \dots N)$
138	137	adantr	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to i : (1 \dots K) ⟶ (1 \dots N)$
139	138	frnd	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to ran i \subseteq (1 \dots N)$
140	124 139	sselpwd	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to ran i \in 𝒫 (1 \dots N)$
141	121 123 112 140	fvmptd	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to F (i) = ran i$
142		simpr	$⊢ (((φ \land i \in A \land j \in A) \land i \neq j) \land z = j) \to z = j$
143	142	rneqd	$⊢ (((φ \land i \in A \land j \in A) \land i \neq j) \land z = j) \to ran z = ran j$
144		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
145	144	3ad2ant1	$⊢ (φ \land i \in A \land j \in A) \to (1 \dots N) \in Fin$
146		eleq1w	$⊢ f = j \to (f \in A \leftrightarrow j \in A)$
147		feq1	$⊢ f = j \to (f : (1 \dots K) ⟶ (1 \dots N) \leftrightarrow j : (1 \dots K) ⟶ (1 \dots N))$
148		fveq1	$⊢ f = j \to f (x) = j (x)$
149		fveq1	$⊢ f = j \to f (y) = j (y)$
150	148 149	breq12d	$⊢ f = j \to (f (x) < f (y) \leftrightarrow j (x) < j (y))$
151	150	imbi2d	$⊢ f = j \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to j (x) < j (y)))$
152	151	2ralbidv	$⊢ f = j \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 j (x) < j (y)))$
153	147 152	anbi12d	$⊢ f = j \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 (j : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to j (x) < j (y))))$
154	146 153	bibi12d	$⊢ f = j \to ((f \in A \leftrightarrow (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 (j \in A \leftrightarrow (j : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to j (x) < j (y)))))$
155	154 20	chvarvv	$⊢ j \in A \leftrightarrow (j : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to j (x) < j (y)))$
156	155	bilani	$⊢ (φ \land j \in A) \to (j : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to j (x) < j (y)))$
157	156	simpld	$⊢ (φ \land j \in A) \to j : (1 \dots K) ⟶ (1 \dots N)$
158	157	3adant2	$⊢ (φ \land i \in A \land j \in A) \to j : (1 \dots K) ⟶ (1 \dots N)$
159	158	frnd	$⊢ (φ \land i \in A \land j \in A) \to ran j \subseteq (1 \dots N)$
160	145 159	sselpwd	$⊢ (φ \land i \in A \land j \in A) \to ran j \in 𝒫 (1 \dots N)$
161	160	adantr	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to ran j \in 𝒫 (1 \dots N)$
162	121 143 113 161	fvmptd	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to F (j) = ran j$
163	120 141 162	3netr4d	$⊢ ((φ \land i \in A \land j \in A) \land i \neq j) \to F (i) \neq F (j)$
164	163	ex	$⊢ (φ \land i \in A \land j \in A) \to (i \neq j \to F (i) \neq F (j))$
165	164	necon4d	$⊢ (φ \land i \in A \land j \in A) \to (F (i) = F (j) \to i = j)$
166	165	3expa	$⊢ ((φ \land i \in A) \land j \in A) \to (F (i) = F (j) \to i = j)$
167	166	ralrimiva	$⊢ (φ \land i \in A) \to \forall j \in A (F (i) = F (j) \to i = j)$
168	167	ralrimiva	$⊢ φ \to \forall i \in A \forall j \in A (F (i) = F (j) \to i = j)$
169	107 168	jca	$⊢ φ \to (F : A ⟶ B \land \forall i \in A \forall j \in A (F (i) = F (j) \to i = j))$
170		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall i \in A \forall j \in A (F (i) = F (j) \to i = j))$
171	169 170	sylibr	$⊢ φ \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem sticksstones2

Proof