Theorem nolt02o 27659

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 1205	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 ∈ No )
2		ltsso 27640	. . . . . 6 ⊢ <s Or No
3		sonr 5563	. . . . . 6 ⊢ (( <s Or No ∧ 𝐴 ∈ No ) → ¬ 𝐴 <s 𝐴)
4	2, 3	mpan 691	. . . . 5 ⊢ (𝐴 ∈ No → ¬ 𝐴 <s 𝐴)
5	1, 4	syl 17	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
6		simp2r 1202	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐵)
7		breq2 5089	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵))
8	6, 7	syl5ibrcom 247	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐴 = 𝐵 → 𝐴 <s 𝐴))
9	5, 8	mtod 198	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 = 𝐵)
10		simpl2l 1228	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
11		simpl11 1250	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 ∈ No )
12		nofun 27613	. . . . . 6 ⊢ (𝐴 ∈ No → Fun 𝐴)
13		funrel 6515	. . . . . 6 ⊢ (Fun 𝐴 → Rel 𝐴)
14	11, 12, 13	3syl 18	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐴)
15		simpl13 1252	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝑋 ∈ On)
16		simpl3 1195	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = ∅)
17		nolt02olem 27658	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
18	11, 15, 16, 17	syl3anc 1374	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
19		relssres 5987	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝑋) → (𝐴 ↾ 𝑋) = 𝐴)
20	14, 18, 19	syl2anc 585	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = 𝐴)
21		simpl12 1251	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐵 ∈ No )
22		nofun 27613	. . . . . 6 ⊢ (𝐵 ∈ No → Fun 𝐵)
23		funrel 6515	. . . . . 6 ⊢ (Fun 𝐵 → Rel 𝐵)
24	21, 22, 23	3syl 18	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐵)
25		simpr 484	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵‘𝑋) = ∅)
26		nolt02olem 27658	. . . . . 6 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋)
27	21, 15, 25, 26	syl3anc 1374	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋)
28		relssres 5987	. . . . 5 ⊢ ((Rel 𝐵 ∧ dom 𝐵 ⊆ 𝑋) → (𝐵 ↾ 𝑋) = 𝐵)
29	24, 27, 28	syl2anc 585	. . . 4 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵 ↾ 𝑋) = 𝐵)
30	10, 20, 29	3eqtr3d 2779	. . 3 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 = 𝐵)
31	9, 30	mtand 816	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = ∅)
32		simp12 1206	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐵 ∈ No )
33		ltsval 27611	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
34	1, 32, 33	syl2anc 585	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
35	6, 34	mpbid 232	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
36		df-an 396	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
37	36	rexbii 3084	. . . . 5 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
38		rexnal 3089	. . . . 5 ⊢ (∃𝑥 ∈ On ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
39	37, 38	bitri 275	. . . 4 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
40	35, 39	sylib 218	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
41		1oex 8415	. . . . . . . . . . . 12 ⊢ 1o ∈ V
42	41	prid1 4706	. . . . . . . . . . 11 ⊢ 1o ∈ {1o, 2o}
43	42	nosgnn0i 27623	. . . . . . . . . 10 ⊢ ∅ ≠ 1o
44	43	neii 2934	. . . . . . . . 9 ⊢ ¬ ∅ = 1o
45		simpll3 1216	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴‘𝑋) = ∅)
46		simplr 769	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐵‘𝑋) = 1o)
47		eqeq1 2740	. . . . . . . . . . . . 13 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → ((𝐴‘𝑋) = ∅ ↔ (𝐵‘𝑋) = ∅))
48	47	anbi1d 632	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) ↔ ((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o)))
49		eqtr2 2757	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ = 1o)
50	48, 49	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ = 1o))
51	50	com12 32	. . . . . . . . . 10 ⊢ (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ = 1o))
52	45, 46, 51	syl2anc 585	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ = 1o))
53	44, 52	mtoi 199	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋) = (𝐵‘𝑋))
54		simpr 484	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → 𝑋 ∈ 𝑥)
55		simplrr 778	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))
56		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → (𝐴‘𝑦) = (𝐴‘𝑋))
57		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → (𝐵‘𝑦) = (𝐵‘𝑋))
58	56, 57	eqeq12d 2752	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘𝑋) = (𝐵‘𝑋)))
59	58	rspcv 3560	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (𝐴‘𝑋) = (𝐵‘𝑋)))
60	54, 55, 59	sylc 65	. . . . . . . 8 ⊢ ((((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → (𝐴‘𝑋) = (𝐵‘𝑋))
61	53, 60	mtand 816	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ 𝑋 ∈ 𝑥)
62		simprl 771	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ∈ On)
63		simpl13 1252	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → 𝑋 ∈ On)
64	63	adantr 480	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑋 ∈ On)
65		ontri1 6357	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥))
66	62, 64, 65	syl2anc 585	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥))
67	61, 66	mpbird 257	. . . . . 6 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ⊆ 𝑋)
68		onsseleq 6364	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)))
69	62, 64, 68	syl2anc 585	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)))
70		eqtr2 2757	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 1o) → ∅ = 1o)
71	70	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) → ∅ = 1o)
72	44, 71	mto 197	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅)
73		df-1o 8405	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
74		df-2o 8406	. . . . . . . . . . . . . . . 16 ⊢ 2o = suc 1o
75	73, 74	eqeq12i 2754	. . . . . . . . . . . . . . 15 ⊢ (1o = 2o ↔ suc ∅ = suc 1o)
76		0elon 6378	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
77		1on 8417	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ On
78		suc11 6432	. . . . . . . . . . . . . . . 16 ⊢ ((∅ ∈ On ∧ 1o ∈ On) → (suc ∅ = suc 1o ↔ ∅ = 1o))
79	76, 77, 78	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ (suc ∅ = suc 1o ↔ ∅ = 1o)
80	75, 79	bitri 275	. . . . . . . . . . . . . 14 ⊢ (1o = 2o ↔ ∅ = 1o)
81	43, 80	nemtbir 3028	. . . . . . . . . . . . 13 ⊢ ¬ 1o = 2o
82		eqtr2 2757	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → 1o = 2o)
83	81, 82	mto 197	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)
84		2on 8418	. . . . . . . . . . . . . . . . 17 ⊢ 2o ∈ On
85	84	elexi 3452	. . . . . . . . . . . . . . . 16 ⊢ 2o ∈ V
86	85	prid2 4707	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ {1o, 2o}
87	86	nosgnn0i 27623	. . . . . . . . . . . . . 14 ⊢ ∅ ≠ 2o
88	87	neii 2934	. . . . . . . . . . . . 13 ⊢ ¬ ∅ = 2o
89		eqtr2 2757	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → ∅ = 2o)
90	88, 89	mto 197	. . . . . . . . . . . 12 ⊢ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)
91	72, 83, 90	3pm3.2i 1341	. . . . . . . . . . 11 ⊢ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))
92		fvex 6853	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↾ 𝑋)‘𝑥) ∈ V
93	92, 92	brtp 5478	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
94		3oran 1109	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
95	93, 94	bitri 275	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)))
96	95	con2bii 357	. . . . . . . . . . 11 ⊢ ((¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥))
97	91, 96	mpbi 230	. . . . . . . . . 10 ⊢ ¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥)
98		simpl2l 1228	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
99	98	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋))
100	99	fveq1d 6842	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥))
101	100	breq2d 5097	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴 ↾ 𝑋)‘𝑥) ↔ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥)))
102	97, 101	mtbii 326	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥))
103		fvres 6859	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥))
104		fvres 6859	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥))
105	103, 104	breq12d 5098	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥) ↔ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
106	105	notbid 318	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋 → (¬ ((𝐴 ↾ 𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘𝑥) ↔ ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
107	102, 106	syl5ibcom 245	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
108	44	intnanr 487	. . . . . . . . . . . 12 ⊢ ¬ (∅ = 1o ∧ 1o = ∅)
109	44	intnanr 487	. . . . . . . . . . . 12 ⊢ ¬ (∅ = 1o ∧ 1o = 2o)
110	81	intnan 486	. . . . . . . . . . . 12 ⊢ ¬ (∅ = ∅ ∧ 1o = 2o)
111	108, 109, 110	3pm3.2i 1341	. . . . . . . . . . 11 ⊢ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o))
112		0ex 5242	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
113	112, 41	brtp 5478	. . . . . . . . . . . . 13 ⊢ (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)))
114		3oran 1109	. . . . . . . . . . . . 13 ⊢ (((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)) ↔ ¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)))
115	113, 114	bitri 275	. . . . . . . . . . . 12 ⊢ (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)))
116	115	con2bii 357	. . . . . . . . . . 11 ⊢ ((¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)) ↔ ¬ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o)
117	111, 116	mpbi 230	. . . . . . . . . 10 ⊢ ¬ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o
118	45, 46	breq12d 5098	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋) ↔ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o))
119	117, 118	mtbiri 327	. . . . . . . . 9 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋))
120		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋))
121		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋))
122	120, 121	breq12d 5098	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋)))
123	122	notbid 318	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑋)))
124	119, 123	syl5ibrcom 247	. . . . . . . 8 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
125	107, 124	jaod 860	. . . . . . 7 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
126	69, 125	sylbid 240	. . . . . 6 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
127	67, 126	mpd 15	. . . . 5 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))
128	127	expr 456	. . . 4 ⊢ (((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
129	128	ralrimiva 3129	. . 3 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
130	40, 129	mtand 816	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = 1o)
131		nofv 27621	. . . 4 ⊢ (𝐵 ∈ No → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o))
132	32, 131	syl 17	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o))
133		3orrot 1092	. . . 4 ⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅))
134		3orrot 1092	. . . 4 ⊢ (((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅) ↔ ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o))
135	133, 134	bitri 275	. . 3 ⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o))
136	132, 135	sylib 218	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o))
137	31, 130, 136	ecase23d 1476	1 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = 2o)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061   ⊆ wss 3889  ∅c0 4273  {ctp 4571  ⟨cop 4573   class class class wbr 5085   Or wor 5538  dom cdm 5631   ↾ cres 5633  Rel wrel 5636  Oncon0 6323  suc csuc 6325  Fun wfun 6492  ‘cfv 6498  1_oc1o 8398  2_oc2o 8399   No csur 27603   <s clts 27604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6326  df-on 6327  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-1o 8405  df-2o 8406  df-no 27606  df-lts 27607

This theorem is referenced by:  nosupbnd1lem4  27675