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

Metamath Proof Explorer

Theorem sticksstones1

Proof