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

Metamath Proof Explorer

Theorem sticksstones2

Proof