nogt01o

Description: Given A greater than B , equal to B up to X , and B ( X ) undefined, then A ( X ) = 1o . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ltsso	$⊢ <_{s} Or No$
2		simp11	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to A \in No$
3		sonr	$⊢ (<_{s} Or No \land A \in No) \to \neg A <_{s} A$
4	1 2 3	sylancr	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to \neg A <_{s} A$
5		simpl2r	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to A <_{s} B$
6		simpl2l	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to {A ↾}_{X} = {B ↾}_{X}$
7		simpl11	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to A \in No$
8		nofun	$⊢ A \in No \to Fun A$
9		funrel	$⊢ Fun A \to Rel A$
10	8 9	syl	$⊢ A \in No \to Rel A$
11	7 10	syl	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to Rel A$
12		simpl13	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to X \in On$
13		simpr	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to A (X) = \emptyset$
14		nolt02olem	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to dom A \subseteq X$
15	7 12 13 14	syl3anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to dom A \subseteq X$
16		relssres	$⊢ (Rel A \land dom A \subseteq X) \to {A ↾}_{X} = A$
17	11 15 16	syl2anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to {A ↾}_{X} = A$
18		simpl12	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to B \in No$
19		nofun	$⊢ B \in No \to Fun B$
20		funrel	$⊢ Fun B \to Rel B$
21	19 20	syl	$⊢ B \in No \to Rel B$
22	18 21	syl	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to Rel B$
23		simpl3	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to B (X) = \emptyset$
24		nolt02olem	$⊢ (B \in No \land X \in On \land B (X) = \emptyset) \to dom B \subseteq X$
25	18 12 23 24	syl3anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to dom B \subseteq X$
26		relssres	$⊢ (Rel B \land dom B \subseteq X) \to {B ↾}_{X} = B$
27	22 25 26	syl2anc	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to {B ↾}_{X} = B$
28	6 17 27	3eqtr3d	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to A = B$
29	5 28	breqtrrd	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = \emptyset) \to A <_{s} A$
30	4 29	mtand	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to \neg A (X) = \emptyset$
31		simp2r	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to A <_{s} B$
32		simp12	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to B \in No$
33		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)))$
34	2 32 33	syl2anc	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (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	31 34	mpbid	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (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		ralinexa	$⊢ \forall x \in On (\forall y \in x A (y) = B (y) \to \neg A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow \neg \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
37	36	con2bii	$⊢ \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))$
38	35 37	sylib	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (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))$
39		1n0	$⊢ 1_{𝑜} \neq \emptyset$
40	39	neii	$⊢ \neg 1_{𝑜} = \emptyset$
41		eqtr2	$⊢ (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset) \to 1_{𝑜} = \emptyset$
42	40 41	mto	$⊢ \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = \emptyset)$
43		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
44		2on	$⊢ 2_{𝑜} \in On$
45	43 44	eqeltrri	$⊢ suc 1_{𝑜} \in On$
46	45	onordi	$⊢ Ord suc 1_{𝑜}$
47		1oex	$⊢ 1_{𝑜} \in V$
48	47	sucid	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
49		nordeq	$⊢ (Ord suc 1_{𝑜} \land 1_{𝑜} \in suc 1_{𝑜}) \to suc 1_{𝑜} \neq 1_{𝑜}$
50	46 48 49	mp2an	$⊢ suc 1_{𝑜} \neq 1_{𝑜}$
51	43 50	eqnetri	$⊢ 2_{𝑜} \neq 1_{𝑜}$
52	51	nesymi	$⊢ \neg 1_{𝑜} = 2_{𝑜}$
53		eqtr2	$⊢ (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜}) \to 1_{𝑜} = 2_{𝑜}$
54	52 53	mto	$⊢ \neg (({A ↾}_{X}) (x) = 1_{𝑜} \land ({A ↾}_{X}) (x) = 2_{𝑜})$
55		2on0	$⊢ 2_{𝑜} \neq \emptyset$
56	55	nesymi	$⊢ \neg \emptyset = 2_{𝑜}$
57		eqtr2	$⊢ (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜}) \to \emptyset = 2_{𝑜}$
58	56 57	mto	$⊢ \neg (({A ↾}_{X}) (x) = \emptyset \land ({A ↾}_{X}) (x) = 2_{𝑜})$
59	42 54 58	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_{𝑜}))$
60		fvex	$⊢ ({A ↾}_{X}) (x) \in V$
61	60 60	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_{𝑜}))$
62		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_{𝑜}))$
63	61 62	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_{𝑜}))$
64	63	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)$
65	59 64	mpbi	$⊢ \neg ({A ↾}_{X}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{X}) (x)$
66		simpl2l	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \to {A ↾}_{X} = {B ↾}_{X}$
67	66	adantr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to {A ↾}_{X} = {B ↾}_{X}$
68	67	fveq1d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to ({A ↾}_{X}) (x) = ({B ↾}_{X}) (x)$
69	68	breq2d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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))$
70	65 69	mtbii	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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)$
71		fvres	$⊢ x \in X \to ({A ↾}_{X}) (x) = A (x)$
72		fvres	$⊢ x \in X \to ({B ↾}_{X}) (x) = B (x)$
73	71 72	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))$
74	73	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))$
75	70 74	syl5ibcom	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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))$
76	51	neii	$⊢ \neg 2_{𝑜} = 1_{𝑜}$
77	76	intnanr	$⊢ \neg (2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset)$
78	56	intnan	$⊢ \neg (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜})$
79	56	intnan	$⊢ \neg (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜})$
80	77 78 79	3pm3.2i	$⊢ (\neg (2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset) \land \neg (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜}) \land \neg (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜}))$
81		2oex	$⊢ 2_{𝑜} \in V$
82		0ex	$⊢ \emptyset \in V$
83	81 82	brtp	$⊢ 2_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset \leftrightarrow ((2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset) \lor (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜}) \lor (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜}))$
84		3oran	$⊢ ((2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset) \lor (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜}) \lor (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜})) \leftrightarrow \neg (\neg (2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset) \land \neg (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜}) \land \neg (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜}))$
85	83 84	bitri	$⊢ 2_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset \leftrightarrow \neg (\neg (2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset) \land \neg (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜}) \land \neg (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜}))$
86	85	con2bii	$⊢ (\neg (2_{𝑜} = 1_{𝑜} \land \emptyset = \emptyset) \land \neg (2_{𝑜} = 1_{𝑜} \land \emptyset = 2_{𝑜}) \land \neg (2_{𝑜} = \emptyset \land \emptyset = 2_{𝑜})) \leftrightarrow \neg 2_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset$
87	80 86	mpbi	$⊢ \neg 2_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset$
88		simplr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to A (X) = 2_{𝑜}$
89		simpll3	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to B (X) = \emptyset$
90	88 89	breq12d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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 2_{𝑜} \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset)$
91	87 90	mtbiri	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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)$
92		fveq2	$⊢ x = X \to A (x) = A (X)$
93		fveq2	$⊢ x = X \to B (x) = B (X)$
94	92 93	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))$
95	94	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))$
96	91 95	syl5ibrcom	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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))$
97		fveq2	$⊢ y = X \to A (y) = A (X)$
98		fveq2	$⊢ y = X \to B (y) = B (X)$
99	97 98	eqeq12d	$⊢ y = X \to (A (y) = B (y) \leftrightarrow A (X) = B (X))$
100	99	rspccv	$⊢ \forall y \in x A (y) = B (y) \to (X \in x \to A (X) = B (X))$
101	100	ad2antll	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (X \in x \to A (X) = B (X))$
102		eqcom	$⊢ A (X) = B (X) \leftrightarrow B (X) = A (X)$
103	101 102	imbitrdi	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (X \in x \to B (X) = A (X))$
104	89 88	eqeq12d	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (B (X) = A (X) \leftrightarrow \emptyset = 2_{𝑜})$
105	103 104	sylibd	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (X \in x \to \emptyset = 2_{𝑜})$
106	56 105	mtoi	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to \neg X \in x$
107		simprl	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to x \in On$
108		simpl13	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \to X \in On$
109	108	adantr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to X \in On$
110		ontri1	$⊢ (x \in On \land X \in On) \to (x \subseteq X \leftrightarrow \neg X \in x)$
111		onsseleq	$⊢ (x \in On \land X \in On) \to (x \subseteq X \leftrightarrow (x \in X \lor x = X))$
112	110 111	bitr3d	$⊢ (x \in On \land X \in On) \to (\neg X \in x \leftrightarrow (x \in X \lor x = X))$
113	107 109 112	syl2anc	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (\neg X \in x \leftrightarrow (x \in X \lor x = X))$
114	106 113	mpbid	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \land (x \in On \land \forall y \in x A (y) = B (y))) \to (x \in X \lor x = X)$
115	75 96 114	mpjaod	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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)$
116	115	expr	$⊢ ((((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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))$
117	116	ralrimiva	$⊢ (((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \land A (X) = 2_{𝑜}) \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))$
118	38 117	mtand	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to \neg A (X) = 2_{𝑜}$
119		nofv	$⊢ A \in No \to (A (X) = \emptyset \lor A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜})$
120	2 119	syl	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to (A (X) = \emptyset \lor A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜})$
121		3orcoma	$⊢ (A (X) = \emptyset \lor A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜}) \leftrightarrow (A (X) = 1_{𝑜} \lor A (X) = \emptyset \lor A (X) = 2_{𝑜})$
122	120 121	sylib	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to (A (X) = 1_{𝑜} \lor A (X) = \emptyset \lor A (X) = 2_{𝑜})$
123	30 118 122	ecase23d	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A <_{s} B) \land B (X) = \emptyset) \to A (X) = 1_{𝑜}$

Metamath Proof Explorer

Theorem nogt01o

Proof