nogesgn1o

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜})) \to B \in No$
2		nofv	$⊢ B \in No \to (B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜})$
3	1 2	syl	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜})) \to (B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜})$
4		3orel2	$⊢ \neg B (X) = 1_{𝑜} \to ((B (X) = \emptyset \lor B (X) = 1_{𝑜} \lor B (X) = 2_{𝑜}) \to (B (X) = \emptyset \lor B (X) = 2_{𝑜}))$
5	3 4	syl5com	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜})) \to (\neg B (X) = 1_{𝑜} \to (B (X) = \emptyset \lor B (X) = 2_{𝑜}))$
6		simp13	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to X \in On$
7		fveq1	$⊢ {A ↾}_{X} = {B ↾}_{X} \to ({A ↾}_{X}) (y) = ({B ↾}_{X}) (y)$
8	7	adantr	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land y \in X) \to ({A ↾}_{X}) (y) = ({B ↾}_{X}) (y)$
9		simpr	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land y \in X) \to y \in X$
10	9	fvresd	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land y \in X) \to ({A ↾}_{X}) (y) = A (y)$
11	9	fvresd	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land y \in X) \to ({B ↾}_{X}) (y) = B (y)$
12	8 10 11	3eqtr3d	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land y \in X) \to A (y) = B (y)$
13	12	ralrimiva	$⊢ {A ↾}_{X} = {B ↾}_{X} \to \forall y \in X A (y) = B (y)$
14	13	adantr	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \to \forall y \in X A (y) = B (y)$
15	14	3ad2ant2	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to \forall y \in X A (y) = B (y)$
16		simp2r	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to A (X) = 1_{𝑜}$
17		simp3	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to (B (X) = \emptyset \lor B (X) = 2_{𝑜})$
18	16 17	jca	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to (A (X) = 1_{𝑜} \land (B (X) = \emptyset \lor B (X) = 2_{𝑜}))$
19		andi	$⊢ (A (X) = 1_{𝑜} \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \leftrightarrow ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}))$
20	18 19	sylib	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}))$
21		3mix1	$⊢ (A (X) = 1_{𝑜} \land B (X) = \emptyset) \to ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}) \lor (A (X) = \emptyset \land B (X) = 2_{𝑜}))$
22		3mix2	$⊢ (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}) \to ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}) \lor (A (X) = \emptyset \land B (X) = 2_{𝑜}))$
23	21 22	jaoi	$⊢ ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜})) \to ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}) \lor (A (X) = \emptyset \land B (X) = 2_{𝑜}))$
24	20 23	syl	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}) \lor (A (X) = \emptyset \land B (X) = 2_{𝑜}))$
25		fvex	$⊢ A (X) \in V$
26		fvex	$⊢ B (X) \in V$
27	25 26	brtp	$⊢ A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X) \leftrightarrow ((A (X) = 1_{𝑜} \land B (X) = \emptyset) \lor (A (X) = 1_{𝑜} \land B (X) = 2_{𝑜}) \lor (A (X) = \emptyset \land B (X) = 2_{𝑜}))$
28	24 27	sylibr	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X)$
29		raleq	$⊢ x = X \to (\forall y \in x A (y) = B (y) \leftrightarrow \forall y \in X A (y) = B (y))$
30		fveq2	$⊢ x = X \to A (x) = A (X)$
31		fveq2	$⊢ x = X \to B (x) = B (X)$
32	30 31	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))$
33	29 32	anbi12d	$⊢ x = X \to ((\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow (\forall y \in X A (y) = B (y) \land A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (X)))$
34	33	rspcev	$⊢ (X \in On \land (\forall y \in X A (y) = B (y) \land A (X) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} 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))$
35	6 15 28 34	syl12anc	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \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		simp11	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to A \in No$
37		simp12	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to B \in No$
38		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)))$
39	36 37 38	syl2anc	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \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)))$
40	35 39	mpbird	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land (B (X) = \emptyset \lor B (X) = 2_{𝑜})) \to A <_{s} B$
41	40	3expia	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜})) \to ((B (X) = \emptyset \lor B (X) = 2_{𝑜}) \to A <_{s} B)$
42	5 41	syld	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜})) \to (\neg B (X) = 1_{𝑜} \to A <_{s} B)$
43	42	con1d	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜})) \to (\neg A <_{s} B \to B (X) = 1_{𝑜})$
44	43	3impia	$⊢ ((A \in No \land B \in No \land X \in On) \land ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \land \neg A <_{s} B) \to B (X) = 1_{𝑜}$

Metamath Proof Explorer

Theorem nogesgn1o

Proof