Theorem sltres

Description: If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011)

	Ref	Expression
Assertion	sltres	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to A{<}_{s}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		noreson	$$⊢\left(A\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to {A\upharpoonright }_X\in \mathrm{No}$$
2	1	3adant2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to {A\upharpoonright }_X\in \mathrm{No}$$
3		noreson	$$⊢\left(B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to {B\upharpoonright }_X\in \mathrm{No}$$
4	3	3adant1	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to {B\upharpoonright }_X\in \mathrm{No}$$
5		sltintdifex	$$⊢\left({A\upharpoonright }_X\in \mathrm{No}\wedge {B\upharpoonright }_X\in \mathrm{No}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{V}\right)$$
6		onintrab	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{V}\leftrightarrow \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}$$
7	5 6	imbitrdi	$$⊢\left({A\upharpoonright }_X\in \mathrm{No}\wedge {B\upharpoonright }_X\in \mathrm{No}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\right)$$
8	2 4 7	syl2anc	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\right)$$
9	8	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}$$
10		simpl3	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to X\in \mathrm{On}$$
11		sltval2	$$⊢\left({A\upharpoonright }_X\in \mathrm{No}\wedge {B\upharpoonright }_X\in \mathrm{No}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\leftrightarrow \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\right)$$
12	2 4 11	syl2anc	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\leftrightarrow \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\right)$$
13		fvex	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{V}$$
14		fvex	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{V}$$
15	13 14	brtp	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\leftrightarrow \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\vee \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)$$
16		1n0	$$⊢1_{𝑜}\ne \varnothing$$
17	16	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
18		eqeq1	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \leftrightarrow 1_{𝑜}=\varnothing \right)$$
19	17 18	mtbiri	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to \neg \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
20		ndmfv	$$⊢\neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
21	19 20	nsyl2	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)$$
22	21	adantr	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)$$
23	22	orcd	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
24	21	adantr	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)$$
25	24	orcd	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
26		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
27	26	elexi	$$⊢2_{𝑜}\in \mathrm{V}$$
28	27	prid2	$$⊢2_{𝑜}\in \left\{1_{𝑜},2_{𝑜}\right\}$$
29	28	nosgnn0i	$$⊢\varnothing \ne 2_{𝑜}$$
30	29	neii	$$⊢\neg \varnothing =2_{𝑜}$$
31		eqeq1	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to \left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \leftrightarrow 2_{𝑜}=\varnothing \right)$$
32		eqcom	$$⊢2_{𝑜}=\varnothing \leftrightarrow \varnothing =2_{𝑜}$$
33	31 32	bitrdi	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to \left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \leftrightarrow \varnothing =2_{𝑜}\right)$$
34	30 33	mtbiri	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to \neg \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
35		ndmfv	$$⊢\neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
36	34 35	nsyl2	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)$$
37	36	adantl	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)$$
38	37	olcd	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
39	23 25 38	3jaoi	$$⊢\left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\vee \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
40	15 39	sylbi	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
41	12 40	syl6bi	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)\right)$$
42	41	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
43		dmres	$$⊢\mathrm{dom}\left({A\upharpoonright }_X\right)=X\cap \mathrm{dom}A$$
44	43	elin2	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\leftrightarrow \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\wedge \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}A\right)$$
45	44	simplbi	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X$$
46		dmres	$$⊢\mathrm{dom}\left({B\upharpoonright }_X\right)=X\cap \mathrm{dom}B$$
47	46	elin2	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\leftrightarrow \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\wedge \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}B\right)$$
48	47	simplbi	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X$$
49	45 48	jaoi	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\vee \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X$$
50	42 49	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X$$
51		onelss	$$⊢X\in \mathrm{On}\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\subseteq X\right)$$
52	10 50 51	sylc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\subseteq X$$
53	52	sselda	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to y\in X$$
54		onelon	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to y\in \mathrm{On}$$
55	9 54	sylan	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to y\in \mathrm{On}$$
56		intss1	$$⊢y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\subseteq y$$
57		ontri1	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\subseteq y\leftrightarrow \neg y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
58	56 57	imbitrid	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to \neg y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
59	58	con2d	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to \neg y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
60	9 59	sylan	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \mathrm{On}\right)\to \left(y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to \neg y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
61	60	impancom	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \left(y\in \mathrm{On}\to \neg y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
62	55 61	mpd	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \neg y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}$$
63		fveq2	$$⊢a=y\to \left({A\upharpoonright }_X\right)\left(a\right)=\left({A\upharpoonright }_X\right)\left(y\right)$$
64		fveq2	$$⊢a=y\to \left({B\upharpoonright }_X\right)\left(a\right)=\left({B\upharpoonright }_X\right)\left(y\right)$$
65	63 64	neeq12d	$$⊢a=y\to \left(\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\leftrightarrow \left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)\right)$$
66	65	elrab	$$⊢y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\leftrightarrow \left(y\in \mathrm{On}\wedge \left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)\right)$$
67	66	simplbi2	$$⊢y\in \mathrm{On}\to \left(\left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)\to y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
68	67	con3d	$$⊢y\in \mathrm{On}\to \left(\neg y\in \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to \neg \left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)\right)$$
69	55 62 68	sylc	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \neg \left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)$$
70		df-ne	$$⊢\left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)\leftrightarrow \neg \left({A\upharpoonright }_X\right)\left(y\right)=\left({B\upharpoonright }_X\right)\left(y\right)$$
71	70	con2bii	$$⊢\left({A\upharpoonright }_X\right)\left(y\right)=\left({B\upharpoonright }_X\right)\left(y\right)\leftrightarrow \neg \left({A\upharpoonright }_X\right)\left(y\right)\ne \left({B\upharpoonright }_X\right)\left(y\right)$$
72	69 71	sylibr	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \left({A\upharpoonright }_X\right)\left(y\right)=\left({B\upharpoonright }_X\right)\left(y\right)$$
73		fvres	$$⊢y\in X\to \left({A\upharpoonright }_X\right)\left(y\right)=A\left(y\right)$$
74		fvres	$$⊢y\in X\to \left({B\upharpoonright }_X\right)\left(y\right)=B\left(y\right)$$
75	73 74	eqeq12d	$$⊢y\in X\to \left(\left({A\upharpoonright }_X\right)\left(y\right)=\left({B\upharpoonright }_X\right)\left(y\right)\leftrightarrow A\left(y\right)=B\left(y\right)\right)$$
76	75	biimpd	$$⊢y\in X\to \left(\left({A\upharpoonright }_X\right)\left(y\right)=\left({B\upharpoonright }_X\right)\left(y\right)\to A\left(y\right)=B\left(y\right)\right)$$
77	53 72 76	sylc	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\wedge y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to A\left(y\right)=B\left(y\right)$$
78	77	ralrimiva	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to \forall y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}A\left(y\right)=B\left(y\right)$$
79		fvresval	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\vee \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)$$
80	79	ori	$$⊢\neg \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
81	19 80	nsyl2	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
82	81	eqcomd	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
83		eqeq2	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\leftrightarrow A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\right)$$
84	82 83	mpbid	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}$$
85	84	adantr	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}$$
86	85	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\right)$$
87	21	ad2antrl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)$$
88	87 45	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X$$
89		nofun	$$⊢{B\upharpoonright }_X\in \mathrm{No}\to \mathrm{Fun}\left({B\upharpoonright }_X\right)$$
90		fvelrn	$$⊢\left(\mathrm{Fun}\left({B\upharpoonright }_X\right)\wedge \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({B\upharpoonright }_X\right)$$
91	90	ex	$$⊢\mathrm{Fun}\left({B\upharpoonright }_X\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({B\upharpoonright }_X\right)\right)$$
92	89 91	syl	$$⊢{B\upharpoonright }_X\in \mathrm{No}\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({B\upharpoonright }_X\right)\right)$$
93		norn	$$⊢{B\upharpoonright }_X\in \mathrm{No}\to \mathrm{ran}\left({B\upharpoonright }_X\right)\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$
94	93	sseld	$$⊢{B\upharpoonright }_X\in \mathrm{No}\to \left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({B\upharpoonright }_X\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
95	92 94	syld	$$⊢{B\upharpoonright }_X\in \mathrm{No}\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
96		nosgnn0	$$⊢\neg \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}$$
97		eleq1	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}\leftrightarrow \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
98	96 97	mtbiri	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \neg \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}$$
99	95 98	nsyli	$$⊢{B\upharpoonright }_X\in \mathrm{No}\to \left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
100	4 99	syl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
101	100	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)$$
102	101	adantrl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)$$
103	47	simplbi2	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}B\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\right)$$
104	103	con3d	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\to \left(\neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}B\right)$$
105	88 102 104	sylc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}B$$
106		ndmfv	$$⊢\neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}B\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
107	105 106	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\right)\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
108	107	ex	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)$$
109	86 108	jcad	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\right)$$
110		fvresval	$$⊢\left(\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\vee \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)$$
111	110	ori	$$⊢\neg \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
112	34 111	nsyl2	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
113	112	eqcomd	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
114		eqeq2	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to \left(B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\leftrightarrow B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)$$
115	113 114	mpbid	$$⊢\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}$$
116	84 115	anim12i	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)$$
117	116	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)$$
118	36	ad2antll	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({B\upharpoonright }_X\right)$$
119	118 48	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X$$
120		nofun	$$⊢{A\upharpoonright }_X\in \mathrm{No}\to \mathrm{Fun}\left({A\upharpoonright }_X\right)$$
121		fvelrn	$$⊢\left(\mathrm{Fun}\left({A\upharpoonright }_X\right)\wedge \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({A\upharpoonright }_X\right)$$
122	121	ex	$$⊢\mathrm{Fun}\left({A\upharpoonright }_X\right)\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({A\upharpoonright }_X\right)\right)$$
123	120 122	syl	$$⊢{A\upharpoonright }_X\in \mathrm{No}\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({A\upharpoonright }_X\right)\right)$$
124		norn	$$⊢{A\upharpoonright }_X\in \mathrm{No}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$
125	124	sseld	$$⊢{A\upharpoonright }_X\in \mathrm{No}\to \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{ran}\left({A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
126	123 125	syld	$$⊢{A\upharpoonright }_X\in \mathrm{No}\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
127		eleq1	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}\leftrightarrow \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
128	96 127	mtbiri	$$⊢\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \neg \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \left\{1_{𝑜},2_{𝑜}\right\}$$
129	126 128	nsyli	$$⊢{A\upharpoonright }_X\in \mathrm{No}\to \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\right)$$
130	2 129	syl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\right)$$
131	130	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)$$
132	131	adantrr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)$$
133	44	simplbi2	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\to \left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}A\to \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\right)$$
134	133	con3d	$$⊢\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in X\to \left(\neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}\left({A\upharpoonright }_X\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}A\right)$$
135	119 132 134	sylc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}A$$
136	135	ex	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}A\right)$$
137		ndmfv	$$⊢\neg \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{dom}A\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing$$
138	136 137	syl6	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)$$
139	115	adantl	$$⊢\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}$$
140	139	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)$$
141	138 140	jcad	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\to \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)$$
142	109 117 141	3orim123d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left(\left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\vee \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge \left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\to \left(\left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)\right)$$
143		fvex	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{V}$$
144		fvex	$$⊢B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\in \mathrm{V}$$
145	143 144	brtp	$$⊢A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\leftrightarrow \left(\left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=1_{𝑜}\wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\vee \left(A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=\varnothing \wedge B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)=2_{𝑜}\right)\right)$$
146	142 15 145	3imtr4g	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}\left({B\upharpoonright }_X\right)\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\right)$$
147	12 146	sylbid	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\right)$$
148	147	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
149		raleq	$$⊢x=\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\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}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}A\left(y\right)=B\left(y\right)\right)$$
150		fveq2	$$⊢x=\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to A\left(x\right)=A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
151		fveq2	$$⊢x=\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\to B\left(x\right)=B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)$$
152	150 151	breq12d	$$⊢x=\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\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}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\right)$$
153	149 152	anbi12d	$$⊢x=\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\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}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}A\left(y\right)=B\left(y\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\right)\right)$$
154	153	rspcev	$$⊢\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\in \mathrm{On}\wedge \left(\forall y\in \bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}A\left(y\right)=B\left(y\right)\wedge A\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\left(a\right)\right\}\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}B\left(\bigcap \left\{a\in \mathrm{On}|\left({A\upharpoonright }_X\right)\left(a\right)\ne \left({B\upharpoonright }_X\right)\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)$$
155	9 78 148 154	syl12anc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\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)$$
156		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)$$
157	156	3adant3	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\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)$$
158	157	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\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)$$
159	155 158	mpbird	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\wedge \left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\right)\to A{<}_{s}B$$
160	159	ex	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge X\in \mathrm{On}\right)\to \left(\left({A\upharpoonright }_X\right){<}_s\left({B\upharpoonright }_X\right)\to A{<}_{s}B\right)$$