Theorem sltval2

Description: Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011)

	Ref	Expression
Assertion	sltval2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{<}_{s}B\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sltval	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{<}_{s}B\leftrightarrow \exists x\in \mathrm{On}\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\right)$$
2		fvex	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\in \mathrm{V}$$
3		fvex	$$⊢B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\in \mathrm{V}$$
4	2 3	brtp	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\leftrightarrow \left(\left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\right)\right)$$
5		1n0	$$⊢1_{𝑜}\ne \varnothing$$
6	5	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
7		eqeq1	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \leftrightarrow 1_{𝑜}=\varnothing \right)$$
8	6 7	mtbiri	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\to \neg A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing$$
9		fvprc	$$⊢\neg \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing$$
10	8 9	nsyl2	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
11	10	adantr	$$⊢\left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
12	10	adantr	$$⊢\left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
13		2on0	$$⊢2_{𝑜}\ne \varnothing$$
14	13	neii	$$⊢\neg 2_{𝑜}=\varnothing$$
15		eqeq1	$$⊢B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\to \left(B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \leftrightarrow 2_{𝑜}=\varnothing \right)$$
16	14 15	mtbiri	$$⊢B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\to \neg B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing$$
17		fvprc	$$⊢\neg \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}\to B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing$$
18	16 17	nsyl2	$$⊢B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
19	18	adantl	$$⊢\left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
20	11 12 19	3jaoi	$$⊢\left(\left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=\varnothing \wedge B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
21	4 20	sylbi	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}$$
22		onintrab	$$⊢\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{V}\leftrightarrow \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
23	21 22	sylib	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
24	23	adantl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
25		onelon	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to y\in \mathrm{On}$$
26	25	expcom	$$⊢y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\to y\in \mathrm{On}\right)$$
27	24 26	syl5	$$⊢y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to y\in \mathrm{On}\right)$$
28		fveq2	$$⊢a=y\to A\left(a\right)=A\left(y\right)$$
29		fveq2	$$⊢a=y\to B\left(a\right)=B\left(y\right)$$
30	28 29	neeq12d	$$⊢a=y\to \left(A\left(a\right)\ne B\left(a\right)\leftrightarrow A\left(y\right)\ne B\left(y\right)\right)$$
31	30	onnminsb	$$⊢y\in \mathrm{On}\to \left(y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \neg A\left(y\right)\ne B\left(y\right)\right)$$
32	31	com12	$$⊢y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(y\in \mathrm{On}\to \neg A\left(y\right)\ne B\left(y\right)\right)$$
33	27 32	syldc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \left(y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \neg A\left(y\right)\ne B\left(y\right)\right)$$
34		df-ne	$$⊢A\left(y\right)\ne B\left(y\right)\leftrightarrow \neg A\left(y\right)=B\left(y\right)$$
35	34	con2bii	$$⊢A\left(y\right)=B\left(y\right)\leftrightarrow \neg A\left(y\right)\ne B\left(y\right)$$
36	33 35	imbitrrdi	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \left(y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to A\left(y\right)=B\left(y\right)\right)$$
37	36	ralrimiv	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)$$
38	24 37	jca	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\right)$$
39	38	ex	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\right)\right)$$
40	39	impac	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \left(\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
41		anass	$$⊢\left(\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\leftrightarrow \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \left(\forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\right)$$
42	40 41	sylib	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \left(\forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\right)$$
43		raleq	$$⊢x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(\forall y\in xA\left(y\right)=B\left(y\right)\leftrightarrow \forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\right)$$
44		fveq2	$$⊢x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to A\left(x\right)=A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
45		fveq2	$$⊢x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to B\left(x\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
46	44 45	breq12d	$$⊢x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
47	43 46	anbi12d	$$⊢x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\leftrightarrow \left(\forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\right)$$
48	47	rspcev	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge \left(\forall y\in \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}A\left(y\right)=B\left(y\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\right)\to \exists x\in \mathrm{On}\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)$$
49	42 48	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\to \exists x\in \mathrm{On}\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)$$
50	49	ex	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \exists x\in \mathrm{On}\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\right)$$
51		eqeq12	$$⊢\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=\varnothing \right)\to \left(A\left(x\right)=B\left(x\right)\leftrightarrow 1_{𝑜}=\varnothing \right)$$
52	6 51	mtbiri	$$⊢\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=\varnothing \right)\to \neg A\left(x\right)=B\left(x\right)$$
53		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
54		0elon	$$⊢\varnothing \in \mathrm{On}$$
55		suc11	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to \left(\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\varnothing \leftrightarrow 1_{𝑜}=\varnothing \right)$$
56	55	necon3bid	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to \left(\mathrm{suc}{1}_{𝑜}\ne \mathrm{suc}\varnothing \leftrightarrow 1_{𝑜}\ne \varnothing \right)$$
57	53 54 56	mp2an	$$⊢\mathrm{suc}{1}_{𝑜}\ne \mathrm{suc}\varnothing \leftrightarrow 1_{𝑜}\ne \varnothing$$
58	5 57	mpbir	$$⊢\mathrm{suc}{1}_{𝑜}\ne \mathrm{suc}\varnothing$$
59		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
60		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
61	59 60	eqeq12i	$$⊢2_{𝑜}=1_{𝑜}\leftrightarrow \mathrm{suc}{1}_{𝑜}=\mathrm{suc}\varnothing$$
62	58 61	nemtbir	$$⊢\neg 2_{𝑜}=1_{𝑜}$$
63		eqeq12	$$⊢\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=2_{𝑜}\right)\to \left(A\left(x\right)=B\left(x\right)\leftrightarrow 1_{𝑜}=2_{𝑜}\right)$$
64		eqcom	$$⊢1_{𝑜}=2_{𝑜}\leftrightarrow 2_{𝑜}=1_{𝑜}$$
65	63 64	bitrdi	$$⊢\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=2_{𝑜}\right)\to \left(A\left(x\right)=B\left(x\right)\leftrightarrow 2_{𝑜}=1_{𝑜}\right)$$
66	62 65	mtbiri	$$⊢\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=2_{𝑜}\right)\to \neg A\left(x\right)=B\left(x\right)$$
67	13	nesymi	$$⊢\neg \varnothing =2_{𝑜}$$
68		eqeq12	$$⊢\left(A\left(x\right)=\varnothing \wedge B\left(x\right)=2_{𝑜}\right)\to \left(A\left(x\right)=B\left(x\right)\leftrightarrow \varnothing =2_{𝑜}\right)$$
69	67 68	mtbiri	$$⊢\left(A\left(x\right)=\varnothing \wedge B\left(x\right)=2_{𝑜}\right)\to \neg A\left(x\right)=B\left(x\right)$$
70	52 66 69	3jaoi	$$⊢\left(\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=\varnothing \right)\vee \left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=2_{𝑜}\right)\vee \left(A\left(x\right)=\varnothing \wedge B\left(x\right)=2_{𝑜}\right)\right)\to \neg A\left(x\right)=B\left(x\right)$$
71		fvex	$$⊢A\left(x\right)\in \mathrm{V}$$
72		fvex	$$⊢B\left(x\right)\in \mathrm{V}$$
73	71 72	brtp	$$⊢A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\leftrightarrow \left(\left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=\varnothing \right)\vee \left(A\left(x\right)=1_{𝑜}\wedge B\left(x\right)=2_{𝑜}\right)\vee \left(A\left(x\right)=\varnothing \wedge B\left(x\right)=2_{𝑜}\right)\right)$$
74		df-ne	$$⊢A\left(x\right)\ne B\left(x\right)\leftrightarrow \neg A\left(x\right)=B\left(x\right)$$
75	70 73 74	3imtr4i	$$⊢A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\to A\left(x\right)\ne B\left(x\right)$$
76		fveq2	$$⊢a=x\to A\left(a\right)=A\left(x\right)$$
77		fveq2	$$⊢a=x\to B\left(a\right)=B\left(x\right)$$
78	76 77	neeq12d	$$⊢a=x\to \left(A\left(a\right)\ne B\left(a\right)\leftrightarrow A\left(x\right)\ne B\left(x\right)\right)$$
79	78	elrab	$$⊢x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\leftrightarrow \left(x\in \mathrm{On}\wedge A\left(x\right)\ne B\left(x\right)\right)$$
80	79	biimpri	$$⊢\left(x\in \mathrm{On}\wedge A\left(x\right)\ne B\left(x\right)\right)\to x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
81	80	adantlr	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\ne B\left(x\right)\right)\to x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
82		ssrab2	$$⊢\left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\subseteq \mathrm{On}$$
83		ne0i	$$⊢x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\ne \varnothing$$
84	83	adantl	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\ne \varnothing$$
85		onint	$$⊢\left(\left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\subseteq \mathrm{On}\wedge \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\ne \varnothing \right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
86	82 84 85	sylancr	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
87		nfrab1	$$⊢\underset{\_}{Ⅎ}a\left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
88	87	nfint	$$⊢\underset{\_}{Ⅎ}a\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
89		nfcv	$$⊢\underset{\_}{Ⅎ}a\mathrm{On}$$
90		nfcv	$$⊢\underset{\_}{Ⅎ}aA$$
91	90 88	nffv	$$⊢\underset{\_}{Ⅎ}aA\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
92		nfcv	$$⊢\underset{\_}{Ⅎ}aB$$
93	92 88	nffv	$$⊢\underset{\_}{Ⅎ}aB\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
94	91 93	nfne	$$⊢ℲaA\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\ne B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
95		fveq2	$$⊢a=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to A\left(a\right)=A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
96		fveq2	$$⊢a=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to B\left(a\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
97	95 96	neeq12d	$$⊢a=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(A\left(a\right)\ne B\left(a\right)\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\ne B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
98	88 89 94 97	elrabf	$$⊢\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\leftrightarrow \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\wedge A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\ne B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
99	98	simprbi	$$⊢\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\ne B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
100	86 99	syl	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\ne B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
101		df-ne	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\ne B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\leftrightarrow \neg A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
102	100 101	sylib	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \neg A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
103		fveq2	$$⊢y=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to A\left(y\right)=A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
104		fveq2	$$⊢y=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to B\left(y\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
105	103 104	eqeq12d	$$⊢y=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \left(A\left(y\right)=B\left(y\right)\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
106	105	rspccv	$$⊢\forall y\in xA\left(y\right)=B\left(y\right)\to \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in x\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
107	106	ad2antlr	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in x\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
108	102 107	mtod	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \neg \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in x$$
109		simpll	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to x\in \mathrm{On}$$
110		oninton	$$⊢\left(\left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\subseteq \mathrm{On}\wedge \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\ne \varnothing \right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
111	82 83 110	sylancr	$$⊢x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
112	111	adantl	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
113		ontri1	$$⊢\left(x\in \mathrm{On}\wedge \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\right)\to \left(x\subseteq \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\leftrightarrow \neg \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in x\right)$$
114	109 112 113	syl2anc	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \left(x\subseteq \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\leftrightarrow \neg \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in x\right)$$
115	108 114	mpbird	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to x\subseteq \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
116		intss1	$$⊢x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\subseteq x$$
117	116	adantl	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\subseteq x$$
118	115 117	eqssd	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge x\in \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\to x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
119	81 118	syldan	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\ne B\left(x\right)\right)\to x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
120	75 119	sylan2	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to x=\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}$$
121	120	fveq2d	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to A\left(x\right)=A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
122	120	fveq2d	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to B\left(x\right)=B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
123	121 122	breq12d	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to \left(A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
124	123	biimpd	$$⊢\left(\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to \left(A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
125	124	ex	$$⊢\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\to \left(A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\to \left(A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)\right)$$
126	125	pm2.43d	$$⊢\left(x\in \mathrm{On}\wedge \forall y\in xA\left(y\right)=B\left(y\right)\right)\to \left(A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
127	126	expimpd	$$⊢x\in \mathrm{On}\to \left(\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$
128	127	rexlimiv	$$⊢\exists x\in \mathrm{On}\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)$$
129	50 128	impbid1	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\leftrightarrow \exists x\in \mathrm{On}\left(\forall y\in xA\left(y\right)=B\left(y\right)\wedge A\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(x\right)\right)\right)$$
130	1 129	bitr4d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{<}_{s}B\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\right)\right)$$