Theorem nolt02o 28098

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

Assertion

Ref	Expression
nolt02o	⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = 2o)

Proof of Theorem nolt02o

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp11 1222	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 ∈ No)
2		ltsso 28079	. . . . . 6 ⊢ <s Or No
3		sonr 5588	. . . . . 6 ⊢ (( <s Or No ∧ 𝐴 ∈ No) → ¬ 𝐴 <s 𝐴)
4	2, 3	mpan 703	. . . . 5 ⊢ (𝐴 ∈ No → ¬ 𝐴 <s 𝐴)
5	1, 4	syl 18	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
6		simp2r 1219	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐵)
7		breq2 5110	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵))
8	6, 7	syl5ibrcom 250	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐴 = 𝐵 → 𝐴 <s 𝐴))
9	5, 8	mtod 201	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 = 𝐵)
10		simpl2l 1245	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
11		simpl11 1267	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 ∈ No)
12		nofun 28052	. . . . . 6 ⊢ (𝐴 ∈ No → Fun 𝐴)
13		funrel 6582	. . . . . 6 ⊢ (Fun 𝐴 → Rel 𝐴)
14	11, 12, 13	3syl 19	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐴)
15		simpl13 1269	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝑋 ∈ On)
16		simpl3 1212	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = ∅)
17		nolt02olem 28097	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
18	11, 15, 16, 17	syl3anc 1399	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
19		relssres 6027	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝑋) → (𝐴 ↾ 𝑋) = 𝐴)
20	14, 18, 19	syl2anc 596	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = 𝐴)
21		simpl12 1268	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐵 ∈ No)
22		nofun 28052	. . . . . 6 ⊢ (𝐵 ∈ No → Fun 𝐵)
23		funrel 6582	. . . . . 6 ⊢ (Fun 𝐵 → Rel 𝐵)
24	21, 22, 23	3syl 19	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐵)
25		simpr 490	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵‘𝑋) = ∅)
26		nolt02olem 28097	. . . . . 6 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋)
27	21, 15, 25, 26	syl3anc 1399	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋)
28		relssres 6027	. . . . 5 ⊢ ((Rel 𝐵 ∧ dom 𝐵 ⊆ 𝑋) → (𝐵 ↾ 𝑋) = 𝐵)
29	24, 27, 28	syl2anc 596	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵 ↾ 𝑋) = 𝐵)
30	10, 20, 29	3eqtr3d 2806	. . 3 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 = 𝐵)
31	9, 30	mtand 828	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = ∅)
32		simp12 1223	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐵 ∈ No)
33		ltsval 28050	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
34	1, 32, 33	syl2anc 596	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
35	6, 34	mpbid 235	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
36		df-an 402	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
37	36	rexbii 3113	. . . . 5 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
38		rexnal 3118	. . . . 5 ⊢ (∃𝑥 ∈ On ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
39	37, 38	bitri 278	. . . 4 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
40	35, 39	sylib 221	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
41		1oex 8522	. . . . . . . . . . . 12 ⊢ 1o ∈ V
42	41	prid1 4723	. . . . . . . . . . 11 ⊢ 1o ∈ {1o, 2o}
43	42	nosgnn0i 28062	. . . . . . . . . 10 ⊢ ∅ ≠ 1o
44	43	neii 2961	. . . . . . . . 9 ⊢ ¬ ∅ = 1o
45		simpll3 1233	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴‘𝑋) = ∅)
46		simplr 781	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐵‘𝑋) = 1o)
47		eqeq1 2767	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → ((𝐴‘𝑋) = ∅ ↔ (𝐵‘𝑋) = ∅))
48	47	anbi1d 643	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) ↔ ((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o)))
49		eqtr2 2784	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ = 1o)
50	48, 49	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ = 1o))
51	50	com12 33	. . . . . . . . . 10 ⊢ (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ = 1o))
52	45, 46, 51	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ = 1o))
53	44, 52	mtoi 202	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋) = (𝐵‘𝑋))
54		simpr 490	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → 𝑋 ∈ 𝑥)
55		simplrr 790	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))
56		fveq2 6914	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → (𝐴‘𝑦) = (𝐴‘𝑋))
57		fveq2 6914	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → (𝐵‘𝑦) = (𝐵‘𝑋))
58	56, 57	eqeq12d 2779	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘𝑋) = (𝐵‘𝑋)))
59	58	rspcv 3576	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (𝐴‘𝑋) = (𝐵‘𝑋)))
60	54, 55, 59	sylc 66	. . . . . . . 8 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → (𝐴‘𝑋) = (𝐵‘𝑋))
61	53, 60	mtand 828	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ 𝑋 ∈ 𝑥)
62		simprl 783	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ∈ On)
63		simpl13 1269	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → 𝑋 ∈ On)
64	63	adantr 486	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑋 ∈ On)
65		ontri1 6421	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥))
66	62, 64, 65	syl2anc 596	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥))
67	61, 66	mpbird 260	. . . . . 6 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ⊆ 𝑋)
68		onsseleq 6428	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)))
69	62, 64, 68	syl2anc 596	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)))
70		eqtr2 2784	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 1o) → ∅ = 1o)
71	70	ancoms 464	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) → ∅ = 1o)
72	44, 71	mto 200	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅)
73		df-1o 8512	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
74		df-2o 8513	. . . . . . . . . . . . . . . 16 ⊢ 2o = suc 1o
75	73, 74	eqeq12i 2781	. . . . . . . . . . . . . . 15 ⊢ (1o = 2o ↔ suc ∅ = suc 1o)
76		0elon 6442	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
77		1on 8525	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
78		suc11 6496	. . . . . . . . . . . . . . . 16 ⊢ ((∅ ∈ On ∧ 1o ∈ On) → (suc ∅ = suc 1o ↔ ∅ = 1o))
79	76, 77, 78	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (suc ∅ = suc 1o ↔ ∅ = 1o)
80	75, 79	bitri 278	. . . . . . . . . . . . . 14 ⊢ (1o = 2o ↔ ∅ = 1o)
81	43, 80	nemtbir 3055	. . . . . . . . . . . . 13 ⊢ ¬ 1o = 2o
82		eqtr2 2784	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → 1o = 2o)
83	81, 82	mto 200	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)
84		2on 8526	. . . . . . . . . . . . . . . . 17 ⊢ 2o ∈ On
85	84	elexi 3476	. . . . . . . . . . . . . . . 16 ⊢ 2o ∈ V
86	85	prid2 4724	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ {1o, 2o}
87	86	nosgnn0i 28062	. . . . . . . . . . . . . 14 ⊢ ∅ ≠ 2o
88	87	neii 2961	. . . . . . . . . . . . 13 ⊢ ¬ ∅ = 2o
89		eqtr2 2784	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → ∅ = 2o)
90	88, 89	mto 200	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)
91	72, 83, 90	3pm3.2i 1358	. . . . . . . . . . 11 ⊢ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))
92		fvex 6927	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↾ 𝑋)‘𝑥) ∈ V
93	92, 92	brtp 5502	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
94		3oran 1126	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
95	93, 94	bitri 278	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
96	95	con2bii 360	. . . . . . . . . . 11 ⊢ ((¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥))
97	91, 96	mpbi 233	. . . . . . . . . 10 ⊢ ¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥)
98		simpl2l 1245	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
99	98	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
100	99	fveq1d 6916	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥))
101	100	breq2d 5118	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥)))
102	97, 101	mtbii 329	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥))
103		fvres 6933	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥))
104		fvres 6933	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥))
105	103, 104	breq12d 5119	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥) ↔ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
106	105	notbid 321	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋 → (¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥) ↔ ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
107	102, 106	syl5ibcom 248	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
108	44	intnanr 493	. . . . . . . . . . . 12 ⊢ ¬ (∅ = 1o ∧ 1o = ∅)
109	44	intnanr 493	. . . . . . . . . . . 12 ⊢ ¬ (∅ = 1o ∧ 1o = 2o)
110	81	intnan 492	. . . . . . . . . . . 12 ⊢ ¬ (∅ = ∅ ∧ 1o = 2o)
111	108, 109, 110	3pm3.2i 1358	. . . . . . . . . . 11 ⊢ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o))
112		0ex 5265	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
113	112, 41	brtp 5502	. . . . . . . . . . . . 13 ⊢ (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)))
114		3oran 1126	. . . . . . . . . . . . 13 ⊢ (((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)) ↔ ¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)))
115	113, 114	bitri 278	. . . . . . . . . . . 12 ⊢ (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)))
116	115	con2bii 360	. . . . . . . . . . 11 ⊢ ((¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)) ↔ ¬ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o)
117	111, 116	mpbi 233	. . . . . . . . . 10 ⊢ ¬ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o
118	45, 46	breq12d 5119	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋) ↔ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o))
119	117, 118	mtbiri 330	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋))
120		fveq2 6914	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋))
121		fveq2 6914	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋))
122	120, 121	breq12d 5119	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋)))
123	122	notbid 321	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋)))
124	119, 123	syl5ibrcom 250	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
125	107, 124	jaod 873	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
126	69, 125	sylbid 243	. . . . . 6 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
127	67, 126	mpd 16	. . . . 5 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))
128	127	expr 462	. . . 4 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
129	128	ralrimiva 3158	. . 3 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
130	40, 129	mtand 828	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = 1o)
131		nofv 28060	. . . 4 ⊢ (𝐵 ∈ No → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o))
132	32, 131	syl 18	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o))
133		3orrot 1108	. . . 4 ⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅))
134		3orrot 1108	. . . 4 ⊢ (((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅) ↔ ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o))
135	133, 134	bitri 278	. . 3 ⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o))
136	132, 135	sylib 221	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o))
137	31, 130, 136	ecase23d 1504	1 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = 2o)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900  ∅c0 4281  {ctp 4592  ⟨cop 4838   class class class wbr 5106   Or wor 5563  dom cdm 5656   ↾ cres 5658  Rel wrel 5661  Oncon0 6386  suc csuc 6388  Fun wfun 6558  ‘cfv 6564  1_oc1o 8505  2_oc2o 8506  Nocsur 28043   <s clts 28044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-fv 6572  df-1o 8512  df-2o 8513  df-no 28046  df-lts 28047

This theorem is used by:  nosupbnd1lem4  28114