nolesgn2ores

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

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

Metamath Proof Explorer

Theorem nolesgn2ores

Proof