nogesgn1ores

Description: Given A greater than or equal to B , equal to B up to X , and A ( X ) = 1o , then ` ( A |`` suc X ) = ( B |`suc X ) . (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Assertion	nogesgn1ores	$⊢ ((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 {A ↾}_{suc X} = {B ↾}_{suc X}$

Proof

Step	Hyp	Ref	Expression
1		dmres	$⊢ dom ({A ↾}_{suc X}) = suc X \cap dom A$
2		simp11	$⊢ ((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 A \in No$
3		nodmord	$⊢ A \in No \to Ord dom A$
4	2 3	syl	$⊢ ((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 Ord dom A$
5		ndmfv	$⊢ \neg X \in dom A \to A (X) = \emptyset$
6		1n0	$⊢ 1_{𝑜} \neq \emptyset$
7	6	necomi	$⊢ \emptyset \neq 1_{𝑜}$
8		neeq1	$⊢ A (X) = \emptyset \to (A (X) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
9	7 8	mpbiri	$⊢ A (X) = \emptyset \to A (X) \neq 1_{𝑜}$
10	9	neneqd	$⊢ A (X) = \emptyset \to \neg A (X) = 1_{𝑜}$
11	5 10	syl	$⊢ \neg X \in dom A \to \neg A (X) = 1_{𝑜}$
12	11	con4i	$⊢ A (X) = 1_{𝑜} \to X \in dom A$
13	12	adantl	$⊢ ({A ↾}_{X} = {B ↾}_{X} \land A (X) = 1_{𝑜}) \to X \in dom A$
14	13	3ad2ant2	$⊢ ((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 X \in dom A$
15		ordsucss	$⊢ Ord dom A \to (X \in dom A \to suc X \subseteq dom A)$
16	4 14 15	sylc	$⊢ ((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 suc X \subseteq dom A$
17		df-ss	$⊢ suc X \subseteq dom A \leftrightarrow suc X \cap dom A = suc X$
18	16 17	sylib	$⊢ ((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 suc X \cap dom A = suc X$
19	1 18	eqtrid	$⊢ ((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 dom ({A ↾}_{suc X}) = suc X$
20		dmres	$⊢ dom ({B ↾}_{suc X}) = suc X \cap dom B$
21		simp12	$⊢ ((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 \in No$
22		nodmord	$⊢ B \in No \to Ord dom B$
23	21 22	syl	$⊢ ((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 Ord dom B$
24		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_{𝑜}$
25		ndmfv	$⊢ \neg X \in dom B \to B (X) = \emptyset$
26		neeq1	$⊢ B (X) = \emptyset \to (B (X) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
27	7 26	mpbiri	$⊢ B (X) = \emptyset \to B (X) \neq 1_{𝑜}$
28	27	neneqd	$⊢ B (X) = \emptyset \to \neg B (X) = 1_{𝑜}$
29	25 28	syl	$⊢ \neg X \in dom B \to \neg B (X) = 1_{𝑜}$
30	29	con4i	$⊢ B (X) = 1_{𝑜} \to X \in dom B$
31	24 30	syl	$⊢ ((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 X \in dom B$
32		ordsucss	$⊢ Ord dom B \to (X \in dom B \to suc X \subseteq dom B)$
33	23 31 32	sylc	$⊢ ((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 suc X \subseteq dom B$
34		df-ss	$⊢ suc X \subseteq dom B \leftrightarrow suc X \cap dom B = suc X$
35	33 34	sylib	$⊢ ((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 suc X \cap dom B = suc X$
36	20 35	eqtrid	$⊢ ((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 dom ({B ↾}_{suc X}) = suc X$
37	19 36	eqtr4d	$⊢ ((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 dom ({A ↾}_{suc X}) = dom ({B ↾}_{suc X})$
38	19	eleq2d	$⊢ ((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 (x \in dom ({A ↾}_{suc X}) \leftrightarrow x \in suc X)$
39		vex	$⊢ x \in V$
40	39	elsuc	$⊢ x \in suc X \leftrightarrow (x \in X \lor x = X)$
41		simpl2l	$⊢ (((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) \land x \in X) \to {A ↾}_{X} = {B ↾}_{X}$
42	41	fveq1d	$⊢ (((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) \land x \in X) \to ({A ↾}_{X}) (x) = ({B ↾}_{X}) (x)$
43		simpr	$⊢ (((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) \land x \in X) \to x \in X$
44	43	fvresd	$⊢ (((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) \land x \in X) \to ({A ↾}_{X}) (x) = A (x)$
45	43	fvresd	$⊢ (((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) \land x \in X) \to ({B ↾}_{X}) (x) = B (x)$
46	42 44 45	3eqtr3d	$⊢ (((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) \land x \in X) \to A (x) = B (x)$
47	46	ex	$⊢ ((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 (x \in X \to A (x) = B (x))$
48		simp2r	$⊢ ((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 A (X) = 1_{𝑜}$
49	48 24	eqtr4d	$⊢ ((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 A (X) = B (X)$
50		fveq2	$⊢ x = X \to A (x) = A (X)$
51		fveq2	$⊢ x = X \to B (x) = B (X)$
52	50 51	eqeq12d	$⊢ x = X \to (A (x) = B (x) \leftrightarrow A (X) = B (X))$
53	49 52	syl5ibrcom	$⊢ ((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 (x = X \to A (x) = B (x))$
54	47 53	jaod	$⊢ ((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 ((x \in X \lor x = X) \to A (x) = B (x))$
55	40 54	syl5bi	$⊢ ((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 (x \in suc X \to A (x) = B (x))$
56	55	imp	$⊢ (((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) \land x \in suc X) \to A (x) = B (x)$
57		simpr	$⊢ (((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) \land x \in suc X) \to x \in suc X$
58	57	fvresd	$⊢ (((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) \land x \in suc X) \to ({A ↾}_{suc X}) (x) = A (x)$
59	57	fvresd	$⊢ (((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) \land x \in suc X) \to ({B ↾}_{suc X}) (x) = B (x)$
60	56 58 59	3eqtr4d	$⊢ (((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) \land x \in suc X) \to ({A ↾}_{suc X}) (x) = ({B ↾}_{suc X}) (x)$
61	60	ex	$⊢ ((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 (x \in suc X \to ({A ↾}_{suc X}) (x) = ({B ↾}_{suc X}) (x))$
62	38 61	sylbid	$⊢ ((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 (x \in dom ({A ↾}_{suc X}) \to ({A ↾}_{suc X}) (x) = ({B ↾}_{suc X}) (x))$
63	62	ralrimiv	$⊢ ((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 \forall x \in dom ({A ↾}_{suc X}) ({A ↾}_{suc X}) (x) = ({B ↾}_{suc X}) (x)$
64		nofun	$⊢ A \in No \to Fun A$
65	2 64	syl	$⊢ ((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 Fun A$
66	65	funresd	$⊢ ((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 Fun ({A ↾}_{suc X})$
67		nofun	$⊢ B \in No \to Fun B$
68	21 67	syl	$⊢ ((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 Fun B$
69	68	funresd	$⊢ ((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 Fun ({B ↾}_{suc X})$
70		eqfunfv	$⊢ (Fun ({A ↾}_{suc X}) \land Fun ({B ↾}_{suc X})) \to ({A ↾}_{suc X} = {B ↾}_{suc X} \leftrightarrow (dom ({A ↾}_{suc X}) = dom ({B ↾}_{suc X}) \land \forall x \in dom ({A ↾}_{suc X}) ({A ↾}_{suc X}) (x) = ({B ↾}_{suc X}) (x)))$
71	66 69 70	syl2anc	$⊢ ((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 ({A ↾}_{suc X} = {B ↾}_{suc X} \leftrightarrow (dom ({A ↾}_{suc X}) = dom ({B ↾}_{suc X}) \land \forall x \in dom ({A ↾}_{suc X}) ({A ↾}_{suc X}) (x) = ({B ↾}_{suc X}) (x)))$
72	37 63 71	mpbir2and	$⊢ ((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 {A ↾}_{suc X} = {B ↾}_{suc X}$

Metamath Proof Explorer

Theorem nogesgn1ores

Proof