Theorem nogt01o

Description: Given A greater than B , equal to B up to X , and B ( X ) undefined, then A ( X ) = 1o . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sltso	⊢ <s Or No
2		simp11	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝐴 ∈ No )
3		sonr	⊢ ( ( <s Or No ∧ 𝐴 ∈ No ) → ¬ 𝐴 <s 𝐴 )
4	1 2 3	sylancr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ¬ 𝐴 <s 𝐴 )
5		simpl2r	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐴 <s 𝐵 )
6		simpl2l	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
7		simpl11	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐴 ∈ No )
8		nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )
9		funrel	⊢ ( Fun 𝐴 → Rel 𝐴 )
10	8 9	syl	⊢ ( 𝐴 ∈ No → Rel 𝐴 )
11	7 10	syl	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → Rel 𝐴 )
12		simpl13	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝑋 ∈ On )
13		simpr	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ‘ 𝑋 ) = ∅ )
14		nolt02olem	⊢ ( ( 𝐴 ∈ No ∧ 𝑋 ∈ On ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → dom 𝐴 ⊆ 𝑋 )
15	7 12 13 14	syl3anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → dom 𝐴 ⊆ 𝑋 )
16		relssres	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝑋 ) → ( 𝐴 ↾ 𝑋 ) = 𝐴 )
17	11 15 16	syl2anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ↾ 𝑋 ) = 𝐴 )
18		simpl12	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐵 ∈ No )
19		nofun	⊢ ( 𝐵 ∈ No → Fun 𝐵 )
20		funrel	⊢ ( Fun 𝐵 → Rel 𝐵 )
21	19 20	syl	⊢ ( 𝐵 ∈ No → Rel 𝐵 )
22	18 21	syl	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → Rel 𝐵 )
23		simpl3	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐵 ‘ 𝑋 ) = ∅ )
24		nolt02olem	⊢ ( ( 𝐵 ∈ No ∧ 𝑋 ∈ On ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → dom 𝐵 ⊆ 𝑋 )
25	18 12 23 24	syl3anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → dom 𝐵 ⊆ 𝑋 )
26		relssres	⊢ ( ( Rel 𝐵 ∧ dom 𝐵 ⊆ 𝑋 ) → ( 𝐵 ↾ 𝑋 ) = 𝐵 )
27	22 25 26	syl2anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐵 ↾ 𝑋 ) = 𝐵 )
28	6 17 27	3eqtr3d	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐴 = 𝐵 )
29	5 28	breqtrrd	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐴 <s 𝐴 )
30	4 29	mtand	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ¬ ( 𝐴 ‘ 𝑋 ) = ∅ )
31		simp2r	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝐴 <s 𝐵 )
32		simp12	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝐵 ∈ No )
33		sltval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
34	2 32 33	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
35	31 34	mpbid	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
36		ralinexa	⊢ ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ¬ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
37	36	con2bii	⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ¬ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
38	35 37	sylib	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ¬ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
39		1n0	⊢ 1o ≠ ∅
40	39	neii	⊢ ¬ 1o = ∅
41		eqtr2	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) → 1o = ∅ )
42	40 41	mto	⊢ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ )
43		df-2o	⊢ 2o = suc 1o
44		2on	⊢ 2o ∈ On
45	43 44	eqeltrri	⊢ suc 1o ∈ On
46	45	onordi	⊢ Ord suc 1o
47		1oex	⊢ 1o ∈ V
48	47	sucid	⊢ 1o ∈ suc 1o
49		nordeq	⊢ ( ( Ord suc 1o ∧ 1o ∈ suc 1o ) → suc 1o ≠ 1o )
50	46 48 49	mp2an	⊢ suc 1o ≠ 1o
51	43 50	eqnetri	⊢ 2o ≠ 1o
52	51	nesymi	⊢ ¬ 1o = 2o
53		eqtr2	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) → 1o = 2o )
54	52 53	mto	⊢ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o )
55		2on0	⊢ 2o ≠ ∅
56	55	nesymi	⊢ ¬ ∅ = 2o
57		eqtr2	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) → ∅ = 2o )
58	56 57	mto	⊢ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o )
59	42 54 58	3pm3.2i	⊢ ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) )
60		fvex	⊢ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ∈ V
61	60 60	brtp	⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) )
62		3oran	⊢ ( ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) ↔ ¬ ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) )
63	61 62	bitri	⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ¬ ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) )
64	63	con2bii	⊢ ( ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) ↔ ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) )
65	59 64	mpbi	⊢ ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 )
66		simpl2l	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
67	66	adantr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
68	67	fveq1d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) )
69	68	breq2d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) ) )
70	65 69	mtbii	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) )
71		fvres	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
72		fvres	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
73	71 72	breq12d	⊢ ( 𝑥 ∈ 𝑋 → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
74	73	notbid	⊢ ( 𝑥 ∈ 𝑋 → ( ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
75	70 74	syl5ibcom	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 ∈ 𝑋 → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
76	51	neii	⊢ ¬ 2o = 1o
77	76	intnanr	⊢ ¬ ( 2o = 1o ∧ ∅ = ∅ )
78	56	intnan	⊢ ¬ ( 2o = 1o ∧ ∅ = 2o )
79	56	intnan	⊢ ¬ ( 2o = ∅ ∧ ∅ = 2o )
80	77 78 79	3pm3.2i	⊢ ( ¬ ( 2o = 1o ∧ ∅ = ∅ ) ∧ ¬ ( 2o = 1o ∧ ∅ = 2o ) ∧ ¬ ( 2o = ∅ ∧ ∅ = 2o ) )
81		2oex	⊢ 2o ∈ V
82		0ex	⊢ ∅ ∈ V
83	81 82	brtp	⊢ ( 2o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅ ↔ ( ( 2o = 1o ∧ ∅ = ∅ ) ∨ ( 2o = 1o ∧ ∅ = 2o ) ∨ ( 2o = ∅ ∧ ∅ = 2o ) ) )
84		3oran	⊢ ( ( ( 2o = 1o ∧ ∅ = ∅ ) ∨ ( 2o = 1o ∧ ∅ = 2o ) ∨ ( 2o = ∅ ∧ ∅ = 2o ) ) ↔ ¬ ( ¬ ( 2o = 1o ∧ ∅ = ∅ ) ∧ ¬ ( 2o = 1o ∧ ∅ = 2o ) ∧ ¬ ( 2o = ∅ ∧ ∅ = 2o ) ) )
85	83 84	bitri	⊢ ( 2o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅ ↔ ¬ ( ¬ ( 2o = 1o ∧ ∅ = ∅ ) ∧ ¬ ( 2o = 1o ∧ ∅ = 2o ) ∧ ¬ ( 2o = ∅ ∧ ∅ = 2o ) ) )
86	85	con2bii	⊢ ( ( ¬ ( 2o = 1o ∧ ∅ = ∅ ) ∧ ¬ ( 2o = 1o ∧ ∅ = 2o ) ∧ ¬ ( 2o = ∅ ∧ ∅ = 2o ) ) ↔ ¬ 2o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅ )
87	80 86	mpbi	⊢ ¬ 2o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅
88		simplr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝐴 ‘ 𝑋 ) = 2o )
89		simpll3	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝐵 ‘ 𝑋 ) = ∅ )
90	88 89	breq12d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) ↔ 2o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅ ) )
91	87 90	mtbiri	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) )
92		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
93		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑋 ) )
94	92 93	breq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) ) )
95	94	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) ) )
96	91 95	syl5ibrcom	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 = 𝑋 → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
97		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑋 ) )
98		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐵 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑋 ) )
99	97 98	eqeq12d	⊢ ( 𝑦 = 𝑋 → ( ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
100	99	rspccv	⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ( 𝑋 ∈ 𝑥 → ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
101	100	ad2antll	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑋 ∈ 𝑥 → ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
102		eqcom	⊢ ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ↔ ( 𝐵 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
103	101 102	syl6ib	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑋 ∈ 𝑥 → ( 𝐵 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) ) )
104	89 88	eqeq12d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐵 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) ↔ ∅ = 2o ) )
105	103 104	sylibd	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑋 ∈ 𝑥 → ∅ = 2o ) )
106	56 105	mtoi	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ 𝑋 ∈ 𝑥 )
107		simprl	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → 𝑥 ∈ On )
108		simpl13	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) → 𝑋 ∈ On )
109	108	adantr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → 𝑋 ∈ On )
110		ontri1	⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ) → ( 𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥 ) )
111		onsseleq	⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ) → ( 𝑥 ⊆ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
112	110 111	bitr3d	⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ) → ( ¬ 𝑋 ∈ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
113	107 109 112	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ¬ 𝑋 ∈ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
114	106 113	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) )
115	75 96 114	mpjaod	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) )
116	115	expr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
117	116	ralrimiva	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) → ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
118	38 117	mtand	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ¬ ( 𝐴 ‘ 𝑋 ) = 2o )
119		nofv	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )
120	2 119	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )
121		3orcoma	⊢ ( ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ↔ ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )
122	120 121	sylib	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )
123	30 118 122	ecase23d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ‘ 𝑋 ) = 1o )