nolesgn2o

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

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

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

Metamath Proof Explorer

Theorem nolesgn2o

Proof