nolesgn2ores - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nolesgn2ores		Structured version Visualization version GIF version

Theorem nolesgn2ores 27579

Description: Given 𝐴 less-than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2_o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.)

**Assertion**
Ref	Expression
nolesgn2ores	⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋))

Proof of Theorem nolesgn2ores Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmres 6001	. . . 4 ⊢ dom (𝐴 ↾ suc 𝑋) = (suc 𝑋 ∩ dom 𝐴)
2		simp11 1201	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → 𝐴 ∈ No )
3		nodmord 27560	. . . . . . 7 ⊢ (𝐴 ∈ No → Ord dom 𝐴)
4	2, 3	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → Ord dom 𝐴)
5		ndmfv 6926	. . . . . . . . . 10 ⊢ (¬ 𝑋 ∈ dom 𝐴 → (𝐴‘𝑋) = ∅)
6		2on 8492	. . . . . . . . . . . . . . 15 ⊢ 2_o ∈ On
7	6	elexi 3489	. . . . . . . . . . . . . 14 ⊢ 2_o ∈ V
8	7	prid2 4763	. . . . . . . . . . . . 13 ⊢ 2_o ∈ {1_o, 2_o}
9	8	nosgnn0i 27566	. . . . . . . . . . . 12 ⊢ ∅ ≠ 2_o
10		neeq1 2998	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑋) = ∅ → ((𝐴‘𝑋) ≠ 2_o ↔ ∅ ≠ 2_o))
11	9, 10	mpbiri 258	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑋) = ∅ → (𝐴‘𝑋) ≠ 2_o)
12	11	neneqd 2940	. . . . . . . . . 10 ⊢ ((𝐴‘𝑋) = ∅ → ¬ (𝐴‘𝑋) = 2_o)
13	5, 12	syl 17	. . . . . . . . 9 ⊢ (¬ 𝑋 ∈ dom 𝐴 → ¬ (𝐴‘𝑋) = 2_o)
14	13	con4i 114	. . . . . . . 8 ⊢ ((𝐴‘𝑋) = 2_o → 𝑋 ∈ dom 𝐴)
15	14	adantl 481	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) → 𝑋 ∈ dom 𝐴)
16	15	3ad2ant2 1132	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → 𝑋 ∈ dom 𝐴)
17		ordsucss 7813	. . . . . 6 ⊢ (Ord dom 𝐴 → (𝑋 ∈ dom 𝐴 → suc 𝑋 ⊆ dom 𝐴))
18	4, 16, 17	sylc 65	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → suc 𝑋 ⊆ dom 𝐴)
19		df-ss 3961	. . . . 5 ⊢ (suc 𝑋 ⊆ dom 𝐴 ↔ (suc 𝑋 ∩ dom 𝐴) = suc 𝑋)
20	18, 19	sylib 217	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (suc 𝑋 ∩ dom 𝐴) = suc 𝑋)
21	1, 20	eqtrid 2779	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → dom (𝐴 ↾ suc 𝑋) = suc 𝑋)
22		dmres 6001	. . . 4 ⊢ dom (𝐵 ↾ suc 𝑋) = (suc 𝑋 ∩ dom 𝐵)
23		simp12 1202	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → 𝐵 ∈ No )
24		nodmord 27560	. . . . . . 7 ⊢ (𝐵 ∈ No → Ord dom 𝐵)
25	23, 24	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → Ord dom 𝐵)
26		nolesgn2o 27578	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝐵‘𝑋) = 2_o)
27		ndmfv 6926	. . . . . . . . 9 ⊢ (¬ 𝑋 ∈ dom 𝐵 → (𝐵‘𝑋) = ∅)
28		neeq1 2998	. . . . . . . . . . 11 ⊢ ((𝐵‘𝑋) = ∅ → ((𝐵‘𝑋) ≠ 2_o ↔ ∅ ≠ 2_o))
29	9, 28	mpbiri 258	. . . . . . . . . 10 ⊢ ((𝐵‘𝑋) = ∅ → (𝐵‘𝑋) ≠ 2_o)
30	29	neneqd 2940	. . . . . . . . 9 ⊢ ((𝐵‘𝑋) = ∅ → ¬ (𝐵‘𝑋) = 2_o)
31	27, 30	syl 17	. . . . . . . 8 ⊢ (¬ 𝑋 ∈ dom 𝐵 → ¬ (𝐵‘𝑋) = 2_o)
32	31	con4i 114	. . . . . . 7 ⊢ ((𝐵‘𝑋) = 2_o → 𝑋 ∈ dom 𝐵)
33	26, 32	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → 𝑋 ∈ dom 𝐵)
34		ordsucss 7813	. . . . . 6 ⊢ (Ord dom 𝐵 → (𝑋 ∈ dom 𝐵 → suc 𝑋 ⊆ dom 𝐵))
35	25, 33, 34	sylc 65	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → suc 𝑋 ⊆ dom 𝐵)
36		df-ss 3961	. . . . 5 ⊢ (suc 𝑋 ⊆ dom 𝐵 ↔ (suc 𝑋 ∩ dom 𝐵) = suc 𝑋)
37	35, 36	sylib 217	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (suc 𝑋 ∩ dom 𝐵) = suc 𝑋)
38	22, 37	eqtrid 2779	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → dom (𝐵 ↾ suc 𝑋) = suc 𝑋)
39	21, 38	eqtr4d 2770	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → dom (𝐴 ↾ suc 𝑋) = dom (𝐵 ↾ suc 𝑋))
40	21	eleq2d 2814	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ dom (𝐴 ↾ suc 𝑋) ↔ 𝑥 ∈ suc 𝑋))
41		vex 3473	. . . . . . . . 9 ⊢ 𝑥 ∈ V
42	41	elsuc 6433	. . . . . . . 8 ⊢ (𝑥 ∈ suc 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))
43		simp2l 1197	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
44	43	fveq1d 6893	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥))
45	44	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥))
46		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
47	46	fvresd 6911	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥))
48	46	fvresd 6911	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥))
49	45, 47, 48	3eqtr3d 2775	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → (𝐴‘𝑥) = (𝐵‘𝑥))
50	49	ex 412	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ 𝑋 → (𝐴‘𝑥) = (𝐵‘𝑥)))
51		simp2r 1198	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴‘𝑋) = 2_o)
52	51, 26	eqtr4d 2770	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴‘𝑋) = (𝐵‘𝑋))
53		fveq2 6891	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋))
54		fveq2 6891	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋))
55	53, 54	eqeq12d 2743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ (𝐴‘𝑋) = (𝐵‘𝑋)))
56	52, 55	syl5ibrcom 246	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐵‘𝑥)))
57	50, 56	jaod 858	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) → (𝐴‘𝑥) = (𝐵‘𝑥)))
58	42, 57	biimtrid 241	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ suc 𝑋 → (𝐴‘𝑥) = (𝐵‘𝑥)))
59	58	imp 406	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → (𝐴‘𝑥) = (𝐵‘𝑥))
60		simpr 484	. . . . . . 7 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → 𝑥 ∈ suc 𝑋)
61	60	fvresd 6911	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → ((𝐴 ↾ suc 𝑋)‘𝑥) = (𝐴‘𝑥))
62	60	fvresd 6911	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → ((𝐵 ↾ suc 𝑋)‘𝑥) = (𝐵‘𝑥))
63	59, 61, 62	3eqtr4d 2777	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → ((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥))
64	63	ex 412	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ suc 𝑋 → ((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥)))
65	40, 64	sylbid 239	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ dom (𝐴 ↾ suc 𝑋) → ((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥)))
66	65	ralrimiv 3140	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → ∀𝑥 ∈ dom (𝐴 ↾ suc 𝑋)((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥))
67		nofun 27556	. . . 4 ⊢ (𝐴 ∈ No → Fun 𝐴)
68		funres 6589	. . . 4 ⊢ (Fun 𝐴 → Fun (𝐴 ↾ suc 𝑋))
69	2, 67, 68	3syl 18	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → Fun (𝐴 ↾ suc 𝑋))
70		nofun 27556	. . . 4 ⊢ (𝐵 ∈ No → Fun 𝐵)
71		funres 6589	. . . 4 ⊢ (Fun 𝐵 → Fun (𝐵 ↾ suc 𝑋))
72	23, 70, 71	3syl 18	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → Fun (𝐵 ↾ suc 𝑋))
73		eqfunfv 7039	. . 3 ⊢ ((Fun (𝐴 ↾ suc 𝑋) ∧ Fun (𝐵 ↾ suc 𝑋)) → ((𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋) ↔ (dom (𝐴 ↾ suc 𝑋) = dom (𝐵 ↾ suc 𝑋) ∧ ∀𝑥 ∈ dom (𝐴 ↾ suc 𝑋)((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥))))
74	69, 72, 73	syl2anc 583	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → ((𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋) ↔ (dom (𝐴 ↾ suc 𝑋) = dom (𝐵 ↾ suc 𝑋) ∧ ∀𝑥 ∈ dom (𝐴 ↾ suc 𝑋)((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥))))
75	39, 66, 74	mpbir2and 712	1 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2_o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 846 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ≠ wne 2935 ∀wral 3056 ∩ cin 3943 ⊆ wss 3944 ∅c0 4318 class class class wbr 5142 dom cdm 5672 ↾ cres 5674 Ord word 6362 Oncon0 6363 suc csuc 6365 Fun wfun 6536 ‘cfv 6542 1_oc1o 8471 2_oc2o 8472 No csur 27547 <s cslt 27548

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pr 5423

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-ral 3057 df-rex 3066 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-ord 6366 df-on 6367 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-1o 8478 df-2o 8479 df-no 27550 df-slt 27551

This theorem is referenced by: nosupbnd1lem3 27617

W3C validator