nolt02o

Description: Given A less than B , equal to B up to X , and undefined at X , then B ( X ) = 2o . (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Assertion	nolt02o	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to B (X) = 2_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		simp11	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to A \in No$
2		sltso	$⊢ <_{s} Or No$
3		sonr	$⊢ (<_{s} Or No \land A \in No) \to \neg A <_{s} A$
4	2 3	mpan	$⊢ A \in No \to \neg A <_{s} A$
5	1 4	syl	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to \neg A <_{s} A$
6		simp2r	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to A <_{s} B$
7		breq2	$⊢ A = B \to (A <_{s} A \leftrightarrow A <_{s} B)$
8	6 7	syl5ibrcom	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to (A = B \to A <_{s} A)$
9	5 8	mtod	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to \neg A = B$
10		simpl2l	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to {A ↾}_{X} = {B ↾}_{X}$
11		simpl11	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to A \in No$
12		nofun	$⊢ A \in No \to Fun A$
13		funrel	$⊢ Fun A \to Rel A$
14	11 12 13	3syl	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to Rel A$
15		simpl13	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to X \in On$
16		simpl3	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to A (X) = \emptyset$
17		nolt02olem	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to dom A \subseteq X$
18	11 15 16 17	syl3anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to dom A \subseteq X$
19		relssres	$⊢ (Rel A \land dom A \subseteq X) \to {A ↾}_{X} = A$
20	14 18 19	syl2anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to {A ↾}_{X} = A$
21		simpl12	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to B \in No$
22		nofun	$⊢ B \in No \to Fun B$
23		funrel	$⊢ Fun B \to Rel B$
24	21 22 23	3syl	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to Rel B$
25		simpr	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to B (X) = \emptyset$
26		nolt02olem	$⊢ (B \in No \land X \in On \land B (X) = \emptyset) \to dom B \subseteq X$
27	21 15 25 26	syl3anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to dom B \subseteq X$
28		relssres	$⊢ (Rel B \land dom B \subseteq X) \to {B ↾}_{X} = B$
29	24 27 28	syl2anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to {B ↾}_{X} = B$
30	10 20 29	3eqtr3d	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = \emptyset) \to A = B$
31	9 30	mtand	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to \neg B (X) = \emptyset$
32		simp12	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to B \in No$
33		sltval	$⊢ (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)))$
34	1 32 33	syl2anc	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \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)))$
35	6 34	mpbid	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
36		df-an	$⊢ (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow \neg (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
37	36	rexbii	$⊢ \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow \exists x \in On \neg (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
38		rexnal	$⊢ \exists x \in On \neg (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow \neg \forall x \in On (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
39	37 38	bitri	$⊢ \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow \neg \forall x \in On (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
40	35 39	sylib	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to \neg \forall x \in On (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
41		1oex	$⊢ 1_{𝑜} \in V$
42	41	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
43	42	nosgnn0i	$⊢ \emptyset \neq 1_{𝑜}$
44	43	neii	$⊢ \neg \emptyset = 1_{𝑜}$
45		simpll3	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to A (X) = \emptyset$
46		simplr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to B (X) = 1_{𝑜}$
47		eqeq1	$⊢ A (X) = B (X) \to (A (X) = \emptyset \leftrightarrow B (X) = \emptyset)$
48	47	anbi1d	$⊢ A (X) = B (X) \to ((A (X) = \emptyset \land B (X) = 1_{𝑜}) \leftrightarrow (B (X) = \emptyset \land B (X) = 1_{𝑜}))$
49		eqtr2	$⊢ (B (X) = \emptyset \land B (X) = 1_{𝑜}) \to \emptyset = 1_{𝑜}$
50	48 49	syl6bi	$⊢ A (X) = B (X) \to ((A (X) = \emptyset \land B (X) = 1_{𝑜}) \to \emptyset = 1_{𝑜})$
51	50	com12	$⊢ (A (X) = \emptyset \land B (X) = 1_{𝑜}) \to (A (X) = B (X) \to \emptyset = 1_{𝑜})$
52	45 46 51	syl2anc	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (A (X) = B (X) \to \emptyset = 1_{𝑜})$
53	44 52	mtoi	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to \neg A (X) = B (X)$
54		simpr	$⊢ (((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \land X \in x) \to X \in x$
55		simplrr	$⊢ (((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \land X \in x) \to \forall y \in x A (y) = B (y)$
56		fveq2	$⊢ y = X \to A (y) = A (X)$
57		fveq2	$⊢ y = X \to B (y) = B (X)$
58	56 57	eqeq12d	$⊢ y = X \to (A (y) = B (y) \leftrightarrow A (X) = B (X))$
59	58	rspcv	$⊢ X \in x \to (\forall y \in x A (y) = B (y) \to A (X) = B (X))$
60	54 55 59	sylc	$⊢ (((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \land X \in x) \to A (X) = B (X)$
61	53 60	mtand	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to \neg X \in x$
62		simprl	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to x \in On$
63		simpl13	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \to X \in On$
64	63	adantr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to X \in On$
65		ontri1	$⊢ (x \in On \land X \in On) \to (x \subseteq X \leftrightarrow \neg X \in x)$
66	62 64 65	syl2anc	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (x \subseteq X \leftrightarrow \neg X \in x)$
67	61 66	mpbird	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to x \subseteq X$
68		onsseleq	$⊢ (x \in On \land X \in On) \to (x \subseteq X \leftrightarrow (x \in X \lor x = X))$
69	62 64 68	syl2anc	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (x \subseteq X \leftrightarrow (x \in X \lor x = X))$
70		eqtr2	$⊢ (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 1_{𝑜}) \to \emptyset = 1_{𝑜}$
71	70	ancoms	$⊢ (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \to \emptyset = 1_{𝑜}$
72	44 71	mto	$⊢ \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset)$
73		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
74		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
75	73 74	eqeq12i	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow suc \emptyset = suc 1_{𝑜}$
76		0elon	$⊢ \emptyset \in On$
77		1on	$⊢ 1_{𝑜} \in On$
78		suc11	$⊢ (\emptyset \in On \land 1_{𝑜} \in On) \to (suc \emptyset = suc 1_{𝑜} \leftrightarrow \emptyset = 1_{𝑜})$
79	76 77 78	mp2an	$⊢ suc \emptyset = suc 1_{𝑜} \leftrightarrow \emptyset = 1_{𝑜}$
80	75 79	bitri	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow \emptyset = 1_{𝑜}$
81	43 80	nemtbir	$⊢ \neg 1_{𝑜} = 2_{𝑜}$
82		eqtr2	$⊢ (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \to 1_{𝑜} = 2_{𝑜}$
83	81 82	mto	$⊢ \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜})$
84		2on	$⊢ 2_{𝑜} \in On$
85	84	elexi	$⊢ 2_{𝑜} \in V$
86	85	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
87	86	nosgnn0i	$⊢ \emptyset \neq 2_{𝑜}$
88	87	neii	$⊢ \neg \emptyset = 2_{𝑜}$
89		eqtr2	$⊢ (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜}) \to \emptyset = 2_{𝑜}$
90	88 89	mto	$⊢ \neg (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜})$
91	72 83 90	3pm3.2i	$⊢ (\neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \land \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \land \neg (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜}))$
92		fvex	$⊢ ({A ↾}_{X}) (x) \in V$
93	92 92	brtp	$⊢ ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{X}) (x) \leftrightarrow ((({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \lor (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \lor (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜}))$
94		3oran	$⊢ ((({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \lor (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \lor (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜})) \leftrightarrow \neg (\neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \land \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \land \neg (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜}))$
95	93 94	bitri	$⊢ ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{X}) (x) \leftrightarrow \neg (\neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \land \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \land \neg (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜}))$
96	95	con2bii	$⊢ (\neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \land \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \land \neg (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜})) \leftrightarrow \neg ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{X}) (x)$
97	91 96	mpbi	$⊢ \neg ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{X}) (x)$
98		simpl2l	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \to {A ↾}_{X} = {B ↾}_{X}$
99	98	adantr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to {A ↾}_{X} = {B ↾}_{X}$
100	99	fveq1d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to ({A ↾}_{X}) (x) = ({B ↾}_{X}) (x)$
101	100	breq2d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{X}) (x) \leftrightarrow ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({B ↾}_{X}) (x))$
102	97 101	mtbii	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to \neg ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({B ↾}_{X}) (x)$
103		fvres	$⊢ x \in X \to ({A ↾}_{X}) (x) = A (x)$
104		fvres	$⊢ x \in X \to ({B ↾}_{X}) (x) = B (x)$
105	103 104	breq12d	$⊢ x \in X \to (({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({B ↾}_{X}) (x) \leftrightarrow A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
106	105	notbid	$⊢ x \in X \to (\neg ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({B ↾}_{X}) (x) \leftrightarrow \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
107	102 106	syl5ibcom	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (x \in X \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
108	44	intnanr	$⊢ \neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset)$
109	44	intnanr	$⊢ \neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜})$
110	81	intnan	$⊢ \neg (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜})$
111	108 109 110	3pm3.2i	$⊢ (\neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset) \land \neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜}) \land \neg (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜}))$
112		0ex	$⊢ \emptyset \in V$
113	112 41	brtp	$⊢ \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} 1_{𝑜} \leftrightarrow ((\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset) \lor (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜}) \lor (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜}))$
114		3oran	$⊢ ((\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset) \lor (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜}) \lor (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜})) \leftrightarrow \neg (\neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset) \land \neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜}) \land \neg (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜}))$
115	113 114	bitri	$⊢ \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} 1_{𝑜} \leftrightarrow \neg (\neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset) \land \neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜}) \land \neg (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜}))$
116	115	con2bii	$⊢ (\neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = \emptyset) \land \neg (\emptyset = 1_{𝑜} \land 1_{𝑜} = 2_{𝑜}) \land \neg (\emptyset = \emptyset \land 1_{𝑜} = 2_{𝑜})) \leftrightarrow \neg \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} 1_{𝑜}$
117	111 116	mpbi	$⊢ \neg \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} 1_{𝑜}$
118	45 46	breq12d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X) \leftrightarrow \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} 1_{𝑜})$
119	117 118	mtbiri	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to \neg A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X)$
120		fveq2	$⊢ x = X \to A (x) = A (X)$
121		fveq2	$⊢ x = X \to B (x) = B (X)$
122	120 121	breq12d	$⊢ x = X \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \leftrightarrow A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X))$
123	122	notbid	$⊢ x = X \to (\neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \leftrightarrow \neg A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X))$
124	119 123	syl5ibrcom	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (x = X \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
125	107 124	jaod	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to ((x \in X \lor x = X) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
126	69 125	sylbid	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (x \subseteq X \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
127	67 126	mpd	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)$
128	127	expr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \land x \in On) \to (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
129	128	ralrimiva	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \land B (X) = 1_{𝑜}) \to \forall x \in On (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
130	40 129	mtand	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to \neg B (X) = 1_{𝑜}$
131		nofv	$⊢ B \in No \to (B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜})$
132	32 131	syl	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to (B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜})$
133		3orrot	$⊢ (B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜}) \leftrightarrow (B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜} \lor B (X) = \emptyset)$
134		3orrot	$⊢ (B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜} \lor B (X) = \emptyset) \leftrightarrow (B (X) = 2_{𝑜} \lor B (X) = \emptyset \lor B (X) = 1_{𝑜})$
135	133 134	bitri	$⊢ (B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜}) \leftrightarrow (B (X) = 2_{𝑜} \lor B (X) = \emptyset \lor B (X) = 1_{𝑜})$
136	132 135	sylib	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to (B (X) = 2_{𝑜} \lor B (X) = \emptyset \lor B (X) = 1_{𝑜})$
137	31 130 136	ecase23d	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land A (X) = \emptyset) \to B (X) = 2_{𝑜}$

Metamath Proof Explorer

Theorem nolt02o

Proof