Theorem nolt02o 27870

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 1221	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 ∈ No )
2		ltsso 27851	. . . . . 6 ⊢ <s Or No
3		sonr 5592	. . . . . 6 ⊢ (( <s Or No ∧ 𝐴 ∈ No ) → ¬ 𝐴 <s 𝐴)
4	2, 3	mpan 702	. . . . 5 ⊢ (𝐴 ∈ No → ¬ 𝐴 <s 𝐴)
5	1, 4	syl 18	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
6		simp2r 1218	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐵)
7		breq2 5112	. . . . 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 1244	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
11		simpl11 1266	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 ∈ No )
12		nofun 27824	. . . . . 6 ⊢ (𝐴 ∈ No → Fun 𝐴)
13		funrel 6553	. . . . . 6 ⊢ (Fun 𝐴 → Rel 𝐴)
14	11, 12, 13	3syl 19	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐴)
15		simpl13 1268	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝑋 ∈ On)
16		simpl3 1211	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = ∅)
17		nolt02olem 27869	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
18	11, 15, 16, 17	syl3anc 1397	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
19		relssres 6020	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝑋) → (𝐴 ↾ 𝑋) = 𝐴)
20	14, 18, 19	syl2anc 595	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = 𝐴)
21		simpl12 1267	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐵 ∈ No )
22		nofun 27824	. . . . . 6 ⊢ (𝐵 ∈ No → Fun 𝐵)
23		funrel 6553	. . . . . 6 ⊢ (Fun 𝐵 → Rel 𝐵)
24	21, 22, 23	3syl 19	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐵)
25		simpr 489	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵‘𝑋) = ∅)
26		nolt02olem 27869	. . . . . 6 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋)
27	21, 15, 25, 26	syl3anc 1397	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋)
28		relssres 6020	. . . . 5 ⊢ ((Rel 𝐵 ∧ dom 𝐵 ⊆ 𝑋) → (𝐵 ↾ 𝑋) = 𝐵)
29	24, 27, 28	syl2anc 595	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵 ↾ 𝑋) = 𝐵)
30	10, 20, 29	3eqtr3d 2805	. . 3 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 = 𝐵)
31	9, 30	mtand 827	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = ∅)
32		simp12 1222	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐵 ∈ No )
33		ltsval 27822	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
34	1, 32, 33	syl2anc 595	. . . . 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 401	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
37	36	rexbii 3111	. . . . 5 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
38		rexnal 3116	. . . . 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 8461	. . . . . . . . . . . 12 ⊢ 1o ∈ V
42	41	prid1 4727	. . . . . . . . . . 11 ⊢ 1o ∈ {1o, 2o}
43	42	nosgnn0i 27834	. . . . . . . . . 10 ⊢ ∅ ≠ 1o
44	43	neii 2959	. . . . . . . . 9 ⊢ ¬ ∅ = 1o
45		simpll3 1232	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴‘𝑋) = ∅)
46		simplr 780	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐵‘𝑋) = 1o)
47		eqeq1 2766	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → ((𝐴‘𝑋) = ∅ ↔ (𝐵‘𝑋) = ∅))
48	47	anbi1d 642	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) ↔ ((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o)))
49		eqtr2 2783	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ = 1o)
50	48, 49	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ = 1o))
51	50	com12 33	. . . . . . . . . 10 ⊢ (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ = 1o))
52	45, 46, 51	syl2anc 595	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ = 1o))
53	44, 52	mtoi 202	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋) = (𝐵‘𝑋))
54		simpr 489	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → 𝑋 ∈ 𝑥)
55		simplrr 789	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))
56		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → (𝐴‘𝑦) = (𝐴‘𝑋))
57		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → (𝐵‘𝑦) = (𝐵‘𝑋))
58	56, 57	eqeq12d 2778	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘𝑋) = (𝐵‘𝑋)))
59	58	rspcv 3576	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (𝐴‘𝑋) = (𝐵‘𝑋)))
60	54, 55, 59	sylc 66	. . . . . . . 8 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → (𝐴‘𝑋) = (𝐵‘𝑋))
61	53, 60	mtand 827	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ 𝑋 ∈ 𝑥)
62		simprl 782	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ∈ On)
63		simpl13 1268	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → 𝑋 ∈ On)
64	63	adantr 485	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑋 ∈ On)
65		ontri1 6395	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥))
66	62, 64, 65	syl2anc 595	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥))
67	61, 66	mpbird 260	. . . . . 6 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ⊆ 𝑋)
68		onsseleq 6402	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)))
69	62, 64, 68	syl2anc 595	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)))
70		eqtr2 2783	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 1o) → ∅ = 1o)
71	70	ancoms 463	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) → ∅ = 1o)
72	44, 71	mto 200	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅)
73		df-1o 8451	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
74		df-2o 8452	. . . . . . . . . . . . . . . 16 ⊢ 2o = suc 1o
75	73, 74	eqeq12i 2780	. . . . . . . . . . . . . . 15 ⊢ (1o = 2o ↔ suc ∅ = suc 1o)
76		0elon 6416	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
77		1on 8464	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
78		suc11 6470	. . . . . . . . . . . . . . . 16 ⊢ ((∅ ∈ On ∧ 1o ∈ On) → (suc ∅ = suc 1o ↔ ∅ = 1o))
79	76, 77, 78	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (suc ∅ = suc 1o ↔ ∅ = 1o)
80	75, 79	bitri 278	. . . . . . . . . . . . . 14 ⊢ (1o = 2o ↔ ∅ = 1o)
81	43, 80	nemtbir 3053	. . . . . . . . . . . . 13 ⊢ ¬ 1o = 2o
82		eqtr2 2783	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → 1o = 2o)
83	81, 82	mto 200	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)
84		2on 8465	. . . . . . . . . . . . . . . . 17 ⊢ 2o ∈ On
85	84	elexi 3476	. . . . . . . . . . . . . . . 16 ⊢ 2o ∈ V
86	85	prid2 4728	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ {1o, 2o}
87	86	nosgnn0i 27834	. . . . . . . . . . . . . 14 ⊢ ∅ ≠ 2o
88	87	neii 2959	. . . . . . . . . . . . 13 ⊢ ¬ ∅ = 2o
89		eqtr2 2783	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → ∅ = 2o)
90	88, 89	mto 200	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)
91	72, 83, 90	3pm3.2i 1357	. . . . . . . . . . 11 ⊢ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))
92		fvex 6894	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↾ 𝑋)‘𝑥) ∈ V
93	92, 92	brtp 5506	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
94		3oran 1125	. . . . . . . . . . . . 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 1244	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
99	98	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
100	99	fveq1d 6883	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥))
101	100	breq2d 5120	. . . . . . . . . 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 6900	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥))
104		fvres 6900	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥))
105	103, 104	breq12d 5121	. . . . . . . . . 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 492	. . . . . . . . . . . 12 ⊢ ¬ (∅ = 1o ∧ 1o = ∅)
109	44	intnanr 492	. . . . . . . . . . . 12 ⊢ ¬ (∅ = 1o ∧ 1o = 2o)
110	81	intnan 491	. . . . . . . . . . . 12 ⊢ ¬ (∅ = ∅ ∧ 1o = 2o)
111	108, 109, 110	3pm3.2i 1357	. . . . . . . . . . 11 ⊢ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o))
112		0ex 5269	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
113	112, 41	brtp 5506	. . . . . . . . . . . . 13 ⊢ (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)))
114		3oran 1125	. . . . . . . . . . . . 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 5121	. . . . . . . . . 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 6881	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋))
121		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋))
122	120, 121	breq12d 5121	. . . . . . . . . 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 872	. . . . . . 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 461	. . . 4 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
129	128	ralrimiva 3156	. . 3 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
130	40, 129	mtand 827	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = 1o)
131		nofv 27832	. . . 4 ⊢ (𝐵 ∈ No → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o))
132	32, 131	syl 18	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o))
133		3orrot 1107	. . . 4 ⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅))
134		3orrot 1107	. . . 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 1502	1 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = 2o)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∨ w3o 1101   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  ∀wral 3078  ∃wrex 3088   ⊆ wss 3904  ∅c0 4285  {ctp 4592  ⟨cop 4594   class class class wbr 5108   Or wor 5567  dom cdm 5660   ↾ cres 5662  Rel wrel 5665  Oncon0 6360  suc csuc 6362  Fun wfun 6530  ‘cfv 6536  1_oc1o 8444  2_oc2o 8445   No csur 27815   <s clts 27816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-ord 6363  df-on 6364  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-1o 8451  df-2o 8452  df-no 27818  df-lts 27819

This theorem is used by:  nosupbnd1lem4  27886