sticksstones1

Description: Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024)

	Ref	Expression
Hypotheses	sticksstones1.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones1.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones1.3	$⊢ 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)))\}$
	sticksstones1.4	$⊢ φ \to X \in A$
	sticksstones1.5	$⊢ φ \to Y \in A$
	sticksstones1.6	$⊢ φ \to X \neq Y$
	sticksstones1.7	$⊢ I = inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <)$
Assertion	sticksstones1	$⊢ φ \to ran X \neq ran Y$

Proof

Step	Hyp	Ref	Expression
1		sticksstones1.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones1.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones1.3	$⊢ 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)))\}$
4		sticksstones1.4	$⊢ φ \to X \in A$
5		sticksstones1.5	$⊢ φ \to Y \in A$
6		sticksstones1.6	$⊢ φ \to X \neq Y$
7		sticksstones1.7	$⊢ I = inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <)$
8	7	a1i	$⊢ φ \to I = inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <)$
9		ltso	$⊢ < Or ℝ$
10	9	a1i	$⊢ φ \to < Or ℝ$
11		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
12		ssrab2	$⊢ \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq (1 \dots K)$
13	12	a1i	$⊢ φ \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq (1 \dots K)$
14		ssfi	$⊢ ((1 \dots K) \in Fin \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq (1 \dots K)) \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin$
15	11 13 14	syl2anc	$⊢ φ \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin$
16		rabeq0	$⊢ \{z \in (1 \dots K) \| X (z) \neq Y (z)\} = \emptyset \leftrightarrow \forall z \in (1 \dots K) \neg X (z) \neq Y (z)$
17		nne	$⊢ \neg X (z) \neq Y (z) \leftrightarrow X (z) = Y (z)$
18	17	ralbii	$⊢ \forall z \in (1 \dots K) \neg X (z) \neq Y (z) \leftrightarrow \forall z \in (1 \dots K) X (z) = Y (z)$
19	16 18	bitri	$⊢ \{z \in (1 \dots K) \| X (z) \neq Y (z)\} = \emptyset \leftrightarrow \forall z \in (1 \dots K) X (z) = Y (z)$
20		feq1	$⊢ f = X \to (f : (1 \dots K) ⟶ (1 \dots N) \leftrightarrow X : (1 \dots K) ⟶ (1 \dots N))$
21		fveq1	$⊢ f = X \to f (x) = X (x)$
22		fveq1	$⊢ f = X \to f (y) = X (y)$
23	21 22	breq12d	$⊢ f = X \to (f (x) < f (y) \leftrightarrow X (x) < X (y))$
24	23	imbi2d	$⊢ f = X \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to X (x) < X (y)))$
25	24	2ralbidv	$⊢ f = X \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 X (x) < X (y)))$
26	20 25	anbi12d	$⊢ f = X \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 (X : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y))))$
27		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))))$
28	3 27	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))))$
29	28	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)))$
30	29	biimpi	$⊢ f \in A \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)))$
31	30	adantl	$⊢ (φ \land f \in A) \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)))$
32	31	ralrimiva	$⊢ φ \to \forall f \in A (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)))$
33	26 32 4	rspcdva	$⊢ φ \to (X : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y)))$
34	33	simpld	$⊢ φ \to X : (1 \dots K) ⟶ (1 \dots N)$
35	34	ffnd	$⊢ φ \to X Fn (1 \dots K)$
36	35	adantr	$⊢ (φ \land \forall z \in (1 \dots K) X (z) = Y (z)) \to X Fn (1 \dots K)$
37		feq1	$⊢ f = Y \to (f : (1 \dots K) ⟶ (1 \dots N) \leftrightarrow Y : (1 \dots K) ⟶ (1 \dots N))$
38		fveq1	$⊢ f = Y \to f (x) = Y (x)$
39		fveq1	$⊢ f = Y \to f (y) = Y (y)$
40	38 39	breq12d	$⊢ f = Y \to (f (x) < f (y) \leftrightarrow Y (x) < Y (y))$
41	40	imbi2d	$⊢ f = Y \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to Y (x) < Y (y)))$
42	41	2ralbidv	$⊢ f = Y \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 Y (x) < Y (y)))$
43	37 42	anbi12d	$⊢ f = Y \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 (Y : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y))))$
44	43 32 5	rspcdva	$⊢ φ \to (Y : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)))$
45	44	adantr	$⊢ (φ \land Y \in A) \to (Y : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)))$
46	5 45	mpdan	$⊢ φ \to (Y : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)))$
47	46	simpld	$⊢ φ \to Y : (1 \dots K) ⟶ (1 \dots N)$
48	47	ffnd	$⊢ φ \to Y Fn (1 \dots K)$
49	48	adantr	$⊢ (φ \land \forall z \in (1 \dots K) X (z) = Y (z)) \to Y Fn (1 \dots K)$
50		eqfnfv	$⊢ (X Fn (1 \dots K) \land Y Fn (1 \dots K)) \to (X = Y \leftrightarrow \forall z \in (1 \dots K) X (z) = Y (z))$
51	36 49 50	syl2anc	$⊢ (φ \land \forall z \in (1 \dots K) X (z) = Y (z)) \to (X = Y \leftrightarrow \forall z \in (1 \dots K) X (z) = Y (z))$
52	51	bicomd	$⊢ (φ \land \forall z \in (1 \dots K) X (z) = Y (z)) \to (\forall z \in (1 \dots K) X (z) = Y (z) \leftrightarrow X = Y)$
53	52	biimpd	$⊢ (φ \land \forall z \in (1 \dots K) X (z) = Y (z)) \to (\forall z \in (1 \dots K) X (z) = Y (z) \to X = Y)$
54	53	syldbl2	$⊢ (φ \land \forall z \in (1 \dots K) X (z) = Y (z)) \to X = Y$
55	19 54	sylan2b	$⊢ (φ \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} = \emptyset) \to X = Y$
56	55	ex	$⊢ φ \to (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} = \emptyset \to X = Y)$
57	56	necon3d	$⊢ φ \to (X \neq Y \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \neq \emptyset)$
58	57	imp	$⊢ (φ \land X \neq Y) \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \neq \emptyset$
59	6 58	mpdan	$⊢ φ \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \neq \emptyset$
60		fz1ssnn	$⊢ (1 \dots K) \subseteq ℕ$
61	60	a1i	$⊢ φ \to (1 \dots K) \subseteq ℕ$
62		nnssre	$⊢ ℕ \subseteq ℝ$
63	62	a1i	$⊢ φ \to ℕ \subseteq ℝ$
64	61 63	sstrd	$⊢ φ \to (1 \dots K) \subseteq ℝ$
65	13 64	sstrd	$⊢ φ \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq ℝ$
66	15 59 65	3jca	$⊢ φ \to (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \neq \emptyset \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq ℝ)$
67		fiinfcl	$⊢ (< Or ℝ \land (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \neq \emptyset \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq ℝ)) \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}$
68	10 66 67	syl2anc	$⊢ φ \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}$
69	8 68	eqeltrd	$⊢ φ \to I \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}$
70	13 68	sseldd	$⊢ φ \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \in (1 \dots K)$
71	8	eleq1d	$⊢ φ \to (I \in (1 \dots K) \leftrightarrow inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \in (1 \dots K))$
72	70 71	mpbird	$⊢ φ \to I \in (1 \dots K)$
73		fveq2	$⊢ z = I \to X (z) = X (I)$
74		fveq2	$⊢ z = I \to Y (z) = Y (I)$
75	73 74	neeq12d	$⊢ z = I \to (X (z) \neq Y (z) \leftrightarrow X (I) \neq Y (I))$
76	75	elrab3	$⊢ I \in (1 \dots K) \to (I \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \leftrightarrow X (I) \neq Y (I))$
77	72 76	syl	$⊢ φ \to (I \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \leftrightarrow X (I) \neq Y (I))$
78	69 77	mpbid	$⊢ φ \to X (I) \neq Y (I)$
79		nfv	$⊢ Ⅎ a φ$
80		nfcv	$⊢ \underline{Ⅎ} a (1 \dots N)$
81		nfcv	$⊢ \underline{Ⅎ} a ℝ$
82		elfznn	$⊢ a \in (1 \dots N) \to a \in ℕ$
83	82	adantl	$⊢ (φ \land a \in (1 \dots N)) \to a \in ℕ$
84		nnre	$⊢ a \in ℕ \to a \in ℝ$
85	83 84	syl	$⊢ (φ \land a \in (1 \dots N)) \to a \in ℝ$
86	85	ex	$⊢ φ \to (a \in (1 \dots N) \to a \in ℝ)$
87	79 80 81 86	ssrd	$⊢ φ \to (1 \dots N) \subseteq ℝ$
88	34 72	ffvelcdmd	$⊢ φ \to X (I) \in (1 \dots N)$
89	87 88	sseldd	$⊢ φ \to X (I) \in ℝ$
90	47 72	ffvelcdmd	$⊢ φ \to Y (I) \in (1 \dots N)$
91	87 90	sseldd	$⊢ φ \to Y (I) \in ℝ$
92		lttri2	$⊢ (X (I) \in ℝ \land Y (I) \in ℝ) \to (X (I) \neq Y (I) \leftrightarrow (X (I) < Y (I) \lor Y (I) < X (I)))$
93	89 91 92	syl2anc	$⊢ φ \to (X (I) \neq Y (I) \leftrightarrow (X (I) < Y (I) \lor Y (I) < X (I)))$
94	78 93	mpbid	$⊢ φ \to (X (I) < Y (I) \lor Y (I) < X (I))$
95	34	ffund	$⊢ φ \to Fun X$
96	95	adantr	$⊢ (φ \land X (I) < Y (I)) \to Fun X$
97	34	fdmd	$⊢ φ \to dom X = (1 \dots K)$
98	72 97	eleqtrrd	$⊢ φ \to I \in dom X$
99	98	adantr	$⊢ (φ \land X (I) < Y (I)) \to I \in dom X$
100		fvelrn	$⊢ (Fun X \land I \in dom X) \to X (I) \in ran X$
101	96 99 100	syl2anc	$⊢ (φ \land X (I) < Y (I)) \to X (I) \in ran X$
102		elfznn	$⊢ j \in (1 \dots K) \to j \in ℕ$
103	102	3ad2ant3	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to j \in ℕ$
104	103	nnred	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to j \in ℝ$
105	64 72	sseldd	$⊢ φ \to I \in ℝ$
106	105	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to I \in ℝ$
107	104 106	lttri4d	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to (j < I \lor j = I \lor I < j)$
108	47	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to Y : (1 \dots K) ⟶ (1 \dots N)$
109		simp3	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to j \in (1 \dots K)$
110	108 109	ffvelcdmd	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to Y (j) \in (1 \dots N)$
111		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
112	111	sseli	$⊢ Y (j) \in (1 \dots N) \to Y (j) \in ℕ$
113		nnre	$⊢ Y (j) \in ℕ \to Y (j) \in ℝ$
114	112 113	syl	$⊢ Y (j) \in (1 \dots N) \to Y (j) \in ℝ$
115	110 114	syl	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to Y (j) \in ℝ$
116	115	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to Y (j) \in ℝ$
117	33	simprd	$⊢ φ \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y))$
118	117	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y))$
119	118	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y))$
120		simpl3	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to j \in (1 \dots K)$
121	72	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to I \in (1 \dots K)$
122	121	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to I \in (1 \dots K)$
123		breq1	$⊢ x = j \to (x < y \leftrightarrow j < y)$
124		fveq2	$⊢ x = j \to X (x) = X (j)$
125	124	breq1d	$⊢ x = j \to (X (x) < X (y) \leftrightarrow X (j) < X (y))$
126	123 125	imbi12d	$⊢ x = j \to ((x < y \to X (x) < X (y)) \leftrightarrow (j < y \to X (j) < X (y)))$
127		breq2	$⊢ y = I \to (j < y \leftrightarrow j < I)$
128		fveq2	$⊢ y = I \to X (y) = X (I)$
129	128	breq2d	$⊢ y = I \to (X (j) < X (y) \leftrightarrow X (j) < X (I))$
130	127 129	imbi12d	$⊢ y = I \to ((j < y \to X (j) < X (y)) \leftrightarrow (j < I \to X (j) < X (I)))$
131	126 130	rspc2v	$⊢ (j \in (1 \dots K) \land I \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y)) \to (j < I \to X (j) < X (I)))$
132	120 122 131	syl2anc	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y)) \to (j < I \to X (j) < X (I)))$
133	119 132	mpd	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to (j < I \to X (j) < X (I))$
134	133	syldbl2	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to X (j) < X (I)$
135		simp2	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to j \in (1 \dots K)$
136		simp3	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to j < I$
137	102	3ad2ant2	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to j \in ℕ$
138	137	nnred	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to j \in ℝ$
139	105	3ad2ant1	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to I \in ℝ$
140	138 139	ltnled	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to (j < I \leftrightarrow \neg I \leq j)$
141	136 140	mpbid	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to \neg I \leq j$
142	65	3ad2ant1	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq ℝ$
143	15	3ad2ant1	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin$
144		infrefilb	$⊢ (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq ℝ \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin \land j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}) \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \leq j$
145	144	3expia	$⊢ (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} \subseteq ℝ \land \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \in Fin) \to (j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \leq j)$
146	142 143 145	syl2anc	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to (j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \leq j)$
147	146	imp	$⊢ ((φ \land j \in (1 \dots K) \land j < I) \land j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}) \to inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \leq j$
148	7	a1i	$⊢ ((φ \land j \in (1 \dots K) \land j < I) \land j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}) \to I = inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <)$
149	148	breq1d	$⊢ ((φ \land j \in (1 \dots K) \land j < I) \land j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}) \to (I \leq j \leftrightarrow inf (\{z \in (1 \dots K) \| X (z) \neq Y (z)\} ℝ <) \leq j)$
150	147 149	mpbird	$⊢ ((φ \land j \in (1 \dots K) \land j < I) \land j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}) \to I \leq j$
151	150	ex	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to (j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \to I \leq j)$
152	151	con3d	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to (\neg I \leq j \to \neg j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\})$
153	141 152	mpd	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to \neg j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\}$
154		nfcv	$⊢ \underline{Ⅎ} z j$
155		nfcv	$⊢ \underline{Ⅎ} z (1 \dots K)$
156		nfv	$⊢ Ⅎ z X (j) \neq Y (j)$
157		fveq2	$⊢ z = j \to X (z) = X (j)$
158		fveq2	$⊢ z = j \to Y (z) = Y (j)$
159	157 158	neeq12d	$⊢ z = j \to (X (z) \neq Y (z) \leftrightarrow X (j) \neq Y (j))$
160	154 155 156 159	elrabf	$⊢ j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \leftrightarrow (j \in (1 \dots K) \land X (j) \neq Y (j))$
161	160	notbii	$⊢ \neg j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \leftrightarrow \neg (j \in (1 \dots K) \land X (j) \neq Y (j))$
162		ianor	$⊢ \neg (j \in (1 \dots K) \land X (j) \neq Y (j)) \leftrightarrow (\neg j \in (1 \dots K) \lor \neg X (j) \neq Y (j))$
163	161 162	bitri	$⊢ \neg j \in \{z \in (1 \dots K) \| X (z) \neq Y (z)\} \leftrightarrow (\neg j \in (1 \dots K) \lor \neg X (j) \neq Y (j))$
164	153 163	sylib	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to (\neg j \in (1 \dots K) \lor \neg X (j) \neq Y (j))$
165		imor	$⊢ (j \in (1 \dots K) \to \neg X (j) \neq Y (j)) \leftrightarrow (\neg j \in (1 \dots K) \lor \neg X (j) \neq Y (j))$
166	164 165	sylibr	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to (j \in (1 \dots K) \to \neg X (j) \neq Y (j))$
167	166	imp	$⊢ ((φ \land j \in (1 \dots K) \land j < I) \land j \in (1 \dots K)) \to \neg X (j) \neq Y (j)$
168		nne	$⊢ \neg X (j) \neq Y (j) \leftrightarrow X (j) = Y (j)$
169	167 168	sylib	$⊢ ((φ \land j \in (1 \dots K) \land j < I) \land j \in (1 \dots K)) \to X (j) = Y (j)$
170	135 169	mpdan	$⊢ (φ \land j \in (1 \dots K) \land j < I) \to X (j) = Y (j)$
171	170	3expa	$⊢ ((φ \land j \in (1 \dots K)) \land j < I) \to X (j) = Y (j)$
172	171	3adantl2	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to X (j) = Y (j)$
173	172	eqcomd	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to Y (j) = X (j)$
174	173	breq1d	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to (Y (j) < X (I) \leftrightarrow X (j) < X (I))$
175	134 174	mpbird	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to Y (j) < X (I)$
176	116 175	ltned	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j < I) \to Y (j) \neq X (I)$
177	78	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to X (I) \neq Y (I)$
178	177	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j = I) \to X (I) \neq Y (I)$
179	178	necomd	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j = I) \to Y (I) \neq X (I)$
180		fveq2	$⊢ j = I \to Y (j) = Y (I)$
181	180	neeq1d	$⊢ j = I \to (Y (j) \neq X (I) \leftrightarrow Y (I) \neq X (I))$
182	181	adantl	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j = I) \to (Y (j) \neq X (I) \leftrightarrow Y (I) \neq X (I))$
183	179 182	mpbird	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land j = I) \to Y (j) \neq X (I)$
184	89	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to X (I) \in ℝ$
185	184	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to X (I) \in ℝ$
186	91	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to Y (I) \in ℝ$
187	186	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to Y (I) \in ℝ$
188	115	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to Y (j) \in ℝ$
189		simpl2	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to X (I) < Y (I)$
190	44	simprd	$⊢ φ \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y))$
191	190	3ad2ant1	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y))$
192	191	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y))$
193	121	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to I \in (1 \dots K)$
194	109	adantr	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to j \in (1 \dots K)$
195		breq1	$⊢ x = I \to (x < y \leftrightarrow I < y)$
196		fveq2	$⊢ x = I \to Y (x) = Y (I)$
197	196	breq1d	$⊢ x = I \to (Y (x) < Y (y) \leftrightarrow Y (I) < Y (y))$
198	195 197	imbi12d	$⊢ x = I \to ((x < y \to Y (x) < Y (y)) \leftrightarrow (I < y \to Y (I) < Y (y)))$
199		breq2	$⊢ y = j \to (I < y \leftrightarrow I < j)$
200		fveq2	$⊢ y = j \to Y (y) = Y (j)$
201	200	breq2d	$⊢ y = j \to (Y (I) < Y (y) \leftrightarrow Y (I) < Y (j))$
202	199 201	imbi12d	$⊢ y = j \to ((I < y \to Y (I) < Y (y)) \leftrightarrow (I < j \to Y (I) < Y (j)))$
203	198 202	rspc2v	$⊢ (I \in (1 \dots K) \land j \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)) \to (I < j \to Y (I) < Y (j)))$
204	193 194 203	syl2anc	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)) \to (I < j \to Y (I) < Y (j)))$
205	192 204	mpd	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to (I < j \to Y (I) < Y (j))$
206	205	syldbl2	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to Y (I) < Y (j)$
207	185 187 188 189 206	lttrd	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to X (I) < Y (j)$
208	185 207	ltned	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to X (I) \neq Y (j)$
209	208	necomd	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land I < j) \to Y (j) \neq X (I)$
210	176 183 209	3jaodan	$⊢ ((φ \land X (I) < Y (I) \land j \in (1 \dots K)) \land (j < I \lor j = I \lor I < j)) \to Y (j) \neq X (I)$
211	107 210	mpdan	$⊢ (φ \land X (I) < Y (I) \land j \in (1 \dots K)) \to Y (j) \neq X (I)$
212	211	3expa	$⊢ ((φ \land X (I) < Y (I)) \land j \in (1 \dots K)) \to Y (j) \neq X (I)$
213	212	neneqd	$⊢ ((φ \land X (I) < Y (I)) \land j \in (1 \dots K)) \to \neg Y (j) = X (I)$
214	213	ralrimiva	$⊢ (φ \land X (I) < Y (I)) \to \forall j \in (1 \dots K) \neg Y (j) = X (I)$
215		ralnex	$⊢ \forall j \in (1 \dots K) \neg Y (j) = X (I) \leftrightarrow \neg \exists j \in (1 \dots K) Y (j) = X (I)$
216	215	a1i	$⊢ φ \to (\forall j \in (1 \dots K) \neg Y (j) = X (I) \leftrightarrow \neg \exists j \in (1 \dots K) Y (j) = X (I))$
217		nnel	$⊢ \neg X (I) \notin ran Y \leftrightarrow X (I) \in ran Y$
218	217	a1i	$⊢ φ \to (\neg X (I) \notin ran Y \leftrightarrow X (I) \in ran Y)$
219		fvelrnb	$⊢ Y Fn (1 \dots K) \to (X (I) \in ran Y \leftrightarrow \exists j \in (1 \dots K) Y (j) = X (I))$
220	48 219	syl	$⊢ φ \to (X (I) \in ran Y \leftrightarrow \exists j \in (1 \dots K) Y (j) = X (I))$
221	218 220	bitrd	$⊢ φ \to (\neg X (I) \notin ran Y \leftrightarrow \exists j \in (1 \dots K) Y (j) = X (I))$
222	221	con1bid	$⊢ φ \to (\neg \exists j \in (1 \dots K) Y (j) = X (I) \leftrightarrow X (I) \notin ran Y)$
223	216 222	bitrd	$⊢ φ \to (\forall j \in (1 \dots K) \neg Y (j) = X (I) \leftrightarrow X (I) \notin ran Y)$
224	223	adantr	$⊢ (φ \land X (I) < Y (I)) \to (\forall j \in (1 \dots K) \neg Y (j) = X (I) \leftrightarrow X (I) \notin ran Y)$
225	214 224	mpbid	$⊢ (φ \land X (I) < Y (I)) \to X (I) \notin ran Y$
226		elnelne1	$⊢ (X (I) \in ran X \land X (I) \notin ran Y) \to ran X \neq ran Y$
227	101 225 226	syl2anc	$⊢ (φ \land X (I) < Y (I)) \to ran X \neq ran Y$
228	47	ffund	$⊢ φ \to Fun Y$
229	228	adantr	$⊢ (φ \land Y (I) < X (I)) \to Fun Y$
230	47	fdmd	$⊢ φ \to dom Y = (1 \dots K)$
231	72 230	eleqtrrd	$⊢ φ \to I \in dom Y$
232	231	adantr	$⊢ (φ \land Y (I) < X (I)) \to I \in dom Y$
233		fvelrn	$⊢ (Fun Y \land I \in dom Y) \to Y (I) \in ran Y$
234	229 232 233	syl2anc	$⊢ (φ \land Y (I) < X (I)) \to Y (I) \in ran Y$
235	102	3ad2ant3	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to j \in ℕ$
236	235	nnred	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to j \in ℝ$
237	105	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to I \in ℝ$
238	236 237	lttri4d	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to (j < I \lor j = I \lor I < j)$
239	34	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to X : (1 \dots K) ⟶ (1 \dots N)$
240		simp3	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to j \in (1 \dots K)$
241	239 240	ffvelcdmd	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to X (j) \in (1 \dots N)$
242	111	sseli	$⊢ X (j) \in (1 \dots N) \to X (j) \in ℕ$
243	241 242	syl	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to X (j) \in ℕ$
244	243	nnred	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to X (j) \in ℝ$
245	244	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to X (j) \in ℝ$
246	190	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y))$
247	246	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y))$
248		simpl3	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to j \in (1 \dots K)$
249	72	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to I \in (1 \dots K)$
250	249	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to I \in (1 \dots K)$
251		fveq2	$⊢ x = j \to Y (x) = Y (j)$
252	251	breq1d	$⊢ x = j \to (Y (x) < Y (y) \leftrightarrow Y (j) < Y (y))$
253	123 252	imbi12d	$⊢ x = j \to ((x < y \to Y (x) < Y (y)) \leftrightarrow (j < y \to Y (j) < Y (y)))$
254		fveq2	$⊢ y = I \to Y (y) = Y (I)$
255	254	breq2d	$⊢ y = I \to (Y (j) < Y (y) \leftrightarrow Y (j) < Y (I))$
256	127 255	imbi12d	$⊢ y = I \to ((j < y \to Y (j) < Y (y)) \leftrightarrow (j < I \to Y (j) < Y (I)))$
257	253 256	rspc2v	$⊢ (j \in (1 \dots K) \land I \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)) \to (j < I \to Y (j) < Y (I)))$
258	248 250 257	syl2anc	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to Y (x) < Y (y)) \to (j < I \to Y (j) < Y (I)))$
259	247 258	mpd	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to (j < I \to Y (j) < Y (I))$
260	259	syldbl2	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to Y (j) < Y (I)$
261	171	3adantl2	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to X (j) = Y (j)$
262	261	breq1d	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to (X (j) < Y (I) \leftrightarrow Y (j) < Y (I))$
263	260 262	mpbird	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to X (j) < Y (I)$
264	245 263	ltned	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j < I) \to X (j) \neq Y (I)$
265	91	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to Y (I) \in ℝ$
266	265	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j = I) \to Y (I) \in ℝ$
267		simpl2	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j = I) \to Y (I) < X (I)$
268	266 267	ltned	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j = I) \to Y (I) \neq X (I)$
269	268	necomd	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j = I) \to X (I) \neq Y (I)$
270		fveq2	$⊢ j = I \to X (j) = X (I)$
271	270	neeq1d	$⊢ j = I \to (X (j) \neq Y (I) \leftrightarrow X (I) \neq Y (I))$
272	271	adantl	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j = I) \to (X (j) \neq Y (I) \leftrightarrow X (I) \neq Y (I))$
273	269 272	mpbird	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land j = I) \to X (j) \neq Y (I)$
274	265	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to Y (I) \in ℝ$
275	89	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to X (I) \in ℝ$
276	275	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to X (I) \in ℝ$
277	244	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to X (j) \in ℝ$
278		simpl2	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to Y (I) < X (I)$
279	117	3ad2ant1	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y))$
280	279	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y))$
281	249	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to I \in (1 \dots K)$
282	240	adantr	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to j \in (1 \dots K)$
283		fveq2	$⊢ x = I \to X (x) = X (I)$
284	283	breq1d	$⊢ x = I \to (X (x) < X (y) \leftrightarrow X (I) < X (y))$
285	195 284	imbi12d	$⊢ x = I \to ((x < y \to X (x) < X (y)) \leftrightarrow (I < y \to X (I) < X (y)))$
286		fveq2	$⊢ y = j \to X (y) = X (j)$
287	286	breq2d	$⊢ y = j \to (X (I) < X (y) \leftrightarrow X (I) < X (j))$
288	199 287	imbi12d	$⊢ y = j \to ((I < y \to X (I) < X (y)) \leftrightarrow (I < j \to X (I) < X (j)))$
289	285 288	rspc2v	$⊢ (I \in (1 \dots K) \land j \in (1 \dots K)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y)) \to (I < j \to X (I) < X (j)))$
290	281 282 289	syl2anc	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to X (x) < X (y)) \to (I < j \to X (I) < X (j)))$
291	280 290	mpd	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to (I < j \to X (I) < X (j))$
292	291	syldbl2	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to X (I) < X (j)$
293	274 276 277 278 292	lttrd	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to Y (I) < X (j)$
294	274 293	ltned	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to Y (I) \neq X (j)$
295	294	necomd	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land I < j) \to X (j) \neq Y (I)$
296	264 273 295	3jaodan	$⊢ ((φ \land Y (I) < X (I) \land j \in (1 \dots K)) \land (j < I \lor j = I \lor I < j)) \to X (j) \neq Y (I)$
297	238 296	mpdan	$⊢ (φ \land Y (I) < X (I) \land j \in (1 \dots K)) \to X (j) \neq Y (I)$
298	297	3expa	$⊢ ((φ \land Y (I) < X (I)) \land j \in (1 \dots K)) \to X (j) \neq Y (I)$
299	298	neneqd	$⊢ ((φ \land Y (I) < X (I)) \land j \in (1 \dots K)) \to \neg X (j) = Y (I)$
300	299	ralrimiva	$⊢ (φ \land Y (I) < X (I)) \to \forall j \in (1 \dots K) \neg X (j) = Y (I)$
301		ralnex	$⊢ \forall j \in (1 \dots K) \neg X (j) = Y (I) \leftrightarrow \neg \exists j \in (1 \dots K) X (j) = Y (I)$
302	301	a1i	$⊢ φ \to (\forall j \in (1 \dots K) \neg X (j) = Y (I) \leftrightarrow \neg \exists j \in (1 \dots K) X (j) = Y (I))$
303		nnel	$⊢ \neg Y (I) \notin ran X \leftrightarrow Y (I) \in ran X$
304	303	a1i	$⊢ φ \to (\neg Y (I) \notin ran X \leftrightarrow Y (I) \in ran X)$
305		fvelrnb	$⊢ X Fn (1 \dots K) \to (Y (I) \in ran X \leftrightarrow \exists j \in (1 \dots K) X (j) = Y (I))$
306	35 305	syl	$⊢ φ \to (Y (I) \in ran X \leftrightarrow \exists j \in (1 \dots K) X (j) = Y (I))$
307	304 306	bitrd	$⊢ φ \to (\neg Y (I) \notin ran X \leftrightarrow \exists j \in (1 \dots K) X (j) = Y (I))$
308	307	con1bid	$⊢ φ \to (\neg \exists j \in (1 \dots K) X (j) = Y (I) \leftrightarrow Y (I) \notin ran X)$
309	302 308	bitrd	$⊢ φ \to (\forall j \in (1 \dots K) \neg X (j) = Y (I) \leftrightarrow Y (I) \notin ran X)$
310	309	adantr	$⊢ (φ \land Y (I) < X (I)) \to (\forall j \in (1 \dots K) \neg X (j) = Y (I) \leftrightarrow Y (I) \notin ran X)$
311	300 310	mpbid	$⊢ (φ \land Y (I) < X (I)) \to Y (I) \notin ran X$
312		elnelne1	$⊢ (Y (I) \in ran Y \land Y (I) \notin ran X) \to ran Y \neq ran X$
313	312	necomd	$⊢ (Y (I) \in ran Y \land Y (I) \notin ran X) \to ran X \neq ran Y$
314	234 311 313	syl2anc	$⊢ (φ \land Y (I) < X (I)) \to ran X \neq ran Y$
315	227 314	jaodan	$⊢ (φ \land (X (I) < Y (I) \lor Y (I) < X (I))) \to ran X \neq ran Y$
316	94 315	mpdan	$⊢ φ \to ran X \neq ran Y$

Metamath Proof Explorer

Theorem sticksstones1

Proof