ltsres

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	ltsres	$⊢ (A \in No \land B \in No \land X \in On) \to (({A ↾}_{X}) <_{s} ({B ↾}_{X}) \to A <_{s} B)$

Proof

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

Metamath Proof Explorer

Theorem ltsres

Proof