Theorem nolt02o

Description: Given A less than B , equal to B up to X , and undefined at X , then B ( X ) = 2o . (Contributed by Scott Fenton, 6-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		simp11	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐴 ∈ No )
2		sltso	⊢ <s Or No
3		sonr	⊢ ( ( <s Or No ∧ 𝐴 ∈ No ) → ¬ 𝐴 <s 𝐴 )
4	2 3	mpan	⊢ ( 𝐴 ∈ No → ¬ 𝐴 <s 𝐴 )
5	1 4	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ¬ 𝐴 <s 𝐴 )
6		simp2r	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐴 <s 𝐵 )
7		breq2	⊢ ( 𝐴 = 𝐵 → ( 𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵 ) )
8	6 7	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐴 = 𝐵 → 𝐴 <s 𝐴 ) )
9	5 8	mtod	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ¬ 𝐴 = 𝐵 )
10		simpl2l	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
11		simpl11	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝐴 ∈ No )
12		nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )
13		funrel	⊢ ( Fun 𝐴 → Rel 𝐴 )
14	11 12 13	3syl	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → Rel 𝐴 )
15		simpl13	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝑋 ∈ On )
16		simpl3	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ‘ 𝑋 ) = ∅ )
17		nolt02olem	⊢ ( ( 𝐴 ∈ No ∧ 𝑋 ∈ On ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → dom 𝐴 ⊆ 𝑋 )
18	11 15 16 17	syl3anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → dom 𝐴 ⊆ 𝑋 )
19		relssres	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝑋 ) → ( 𝐴 ↾ 𝑋 ) = 𝐴 )
20	14 18 19	syl2anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐴 ↾ 𝑋 ) = 𝐴 )
21		simpl12	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝐵 ∈ No )
22		nofun	⊢ ( 𝐵 ∈ No → Fun 𝐵 )
23		funrel	⊢ ( Fun 𝐵 → Rel 𝐵 )
24	21 22 23	3syl	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → Rel 𝐵 )
25		simpr	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐵 ‘ 𝑋 ) = ∅ )
26		nolt02olem	⊢ ( ( 𝐵 ∈ No ∧ 𝑋 ∈ On ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → dom 𝐵 ⊆ 𝑋 )
27	21 15 25 26	syl3anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → dom 𝐵 ⊆ 𝑋 )
28		relssres	⊢ ( ( Rel 𝐵 ∧ dom 𝐵 ⊆ 𝑋 ) → ( 𝐵 ↾ 𝑋 ) = 𝐵 )
29	24 27 28	syl2anc	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → ( 𝐵 ↾ 𝑋 ) = 𝐵 )
30	10 20 29	3eqtr3d	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = ∅ ) → 𝐴 = 𝐵 )
31	9 30	mtand	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ¬ ( 𝐵 ‘ 𝑋 ) = ∅ )
32		simp12	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → 𝐵 ∈ No )
33		sltval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
34	1 32 33	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
35	6 34	mpbid	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
36		df-an	⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ¬ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
37	36	rexbii	⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ¬ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
38		rexnal	⊢ ( ∃ 𝑥 ∈ On ¬ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ¬ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
39	37 38	bitri	⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ¬ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
40	35 39	sylib	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ¬ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
41		1oex	⊢ 1o ∈ V
42	41	prid1	⊢ 1o ∈ { 1o , 2o }
43	42	nosgnn0i	⊢ ∅ ≠ 1o
44	43	neii	⊢ ¬ ∅ = 1o
45		simpll3	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝐴 ‘ 𝑋 ) = ∅ )
46		simplr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝐵 ‘ 𝑋 ) = 1o )
47		eqeq1	⊢ ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) → ( ( 𝐴 ‘ 𝑋 ) = ∅ ↔ ( 𝐵 ‘ 𝑋 ) = ∅ ) )
48	47	anbi1d	⊢ ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) → ( ( ( 𝐴 ‘ 𝑋 ) = ∅ ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ↔ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ) )
49		eqtr2	⊢ ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) → ∅ = 1o )
50	48 49	syl6bi	⊢ ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) → ( ( ( 𝐴 ‘ 𝑋 ) = ∅ ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) → ∅ = 1o ) )
51	50	com12	⊢ ( ( ( 𝐴 ‘ 𝑋 ) = ∅ ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) → ∅ = 1o ) )
52	45 46 51	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) → ∅ = 1o ) )
53	44 52	mtoi	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) )
54		simpr	⊢ ( ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) ∧ 𝑋 ∈ 𝑥 ) → 𝑋 ∈ 𝑥 )
55		simplrr	⊢ ( ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) ∧ 𝑋 ∈ 𝑥 ) → ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
56		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑋 ) )
57		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐵 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑋 ) )
58	56 57	eqeq12d	⊢ ( 𝑦 = 𝑋 → ( ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
59	58	rspcv	⊢ ( 𝑋 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
60	54 55 59	sylc	⊢ ( ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) ∧ 𝑋 ∈ 𝑥 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) )
61	53 60	mtand	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ 𝑋 ∈ 𝑥 )
62		simprl	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → 𝑥 ∈ On )
63		simpl13	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) → 𝑋 ∈ On )
64	63	adantr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → 𝑋 ∈ On )
65		ontri1	⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ) → ( 𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥 ) )
66	62 64 65	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥 ) )
67	61 66	mpbird	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → 𝑥 ⊆ 𝑋 )
68		onsseleq	⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ) → ( 𝑥 ⊆ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
69	62 64 68	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 ⊆ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
70		eqtr2	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ) → ∅ = 1o )
71	70	ancoms	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) → ∅ = 1o )
72	44 71	mto	⊢ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ )
73		df-1o	⊢ 1o = suc ∅
74		df-2o	⊢ 2o = suc 1o
75	73 74	eqeq12i	⊢ ( 1o = 2o ↔ suc ∅ = suc 1o )
76		0elon	⊢ ∅ ∈ On
77		1on	⊢ 1o ∈ On
78		suc11	⊢ ( ( ∅ ∈ On ∧ 1o ∈ On ) → ( suc ∅ = suc 1o ↔ ∅ = 1o ) )
79	76 77 78	mp2an	⊢ ( suc ∅ = suc 1o ↔ ∅ = 1o )
80	75 79	bitri	⊢ ( 1o = 2o ↔ ∅ = 1o )
81	43 80	nemtbir	⊢ ¬ 1o = 2o
82		eqtr2	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) → 1o = 2o )
83	81 82	mto	⊢ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o )
84		2on	⊢ 2o ∈ On
85	84	elexi	⊢ 2o ∈ V
86	85	prid2	⊢ 2o ∈ { 1o , 2o }
87	86	nosgnn0i	⊢ ∅ ≠ 2o
88	87	neii	⊢ ¬ ∅ = 2o
89		eqtr2	⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) → ∅ = 2o )
90	88 89	mto	⊢ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o )
91	72 83 90	3pm3.2i	⊢ ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) )
92		fvex	⊢ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ∈ V
93	92 92	brtp	⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) )
94		3oran	⊢ ( ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) ↔ ¬ ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) )
95	93 94	bitri	⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ¬ ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) )
96	95	con2bii	⊢ ( ( ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 1o ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ∧ ¬ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ∅ ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = 2o ) ) ↔ ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) )
97	91 96	mpbi	⊢ ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 )
98		simpl2l	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
99	98	adantr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
100	99	fveq1d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) )
101	100	breq2d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) ) )
102	97 101	mtbii	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) )
103		fvres	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
104		fvres	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
105	103 104	breq12d	⊢ ( 𝑥 ∈ 𝑋 → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
106	105	notbid	⊢ ( 𝑥 ∈ 𝑋 → ( ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
107	102 106	syl5ibcom	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 ∈ 𝑋 → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
108	44	intnanr	⊢ ¬ ( ∅ = 1o ∧ 1o = ∅ )
109	44	intnanr	⊢ ¬ ( ∅ = 1o ∧ 1o = 2o )
110	81	intnan	⊢ ¬ ( ∅ = ∅ ∧ 1o = 2o )
111	108 109 110	3pm3.2i	⊢ ( ¬ ( ∅ = 1o ∧ 1o = ∅ ) ∧ ¬ ( ∅ = 1o ∧ 1o = 2o ) ∧ ¬ ( ∅ = ∅ ∧ 1o = 2o ) )
112		0ex	⊢ ∅ ∈ V
113	112 41	brtp	⊢ ( ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 1o ↔ ( ( ∅ = 1o ∧ 1o = ∅ ) ∨ ( ∅ = 1o ∧ 1o = 2o ) ∨ ( ∅ = ∅ ∧ 1o = 2o ) ) )
114		3oran	⊢ ( ( ( ∅ = 1o ∧ 1o = ∅ ) ∨ ( ∅ = 1o ∧ 1o = 2o ) ∨ ( ∅ = ∅ ∧ 1o = 2o ) ) ↔ ¬ ( ¬ ( ∅ = 1o ∧ 1o = ∅ ) ∧ ¬ ( ∅ = 1o ∧ 1o = 2o ) ∧ ¬ ( ∅ = ∅ ∧ 1o = 2o ) ) )
115	113 114	bitri	⊢ ( ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 1o ↔ ¬ ( ¬ ( ∅ = 1o ∧ 1o = ∅ ) ∧ ¬ ( ∅ = 1o ∧ 1o = 2o ) ∧ ¬ ( ∅ = ∅ ∧ 1o = 2o ) ) )
116	115	con2bii	⊢ ( ( ¬ ( ∅ = 1o ∧ 1o = ∅ ) ∧ ¬ ( ∅ = 1o ∧ 1o = 2o ) ∧ ¬ ( ∅ = ∅ ∧ 1o = 2o ) ) ↔ ¬ ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 1o )
117	111 116	mpbi	⊢ ¬ ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 1o
118	45 46	breq12d	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) ↔ ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 1o ) )
119	117 118	mtbiri	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) )
120		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
121		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑋 ) )
122	120 121	breq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) ) )
123	122	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑋 ) ) )
124	119 123	syl5ibrcom	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 = 𝑋 → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
125	107 124	jaod	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
126	69 125	sylbid	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ( 𝑥 ⊆ 𝑋 → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
127	67 126	mpd	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) )
128	127	expr	⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
129	128	ralrimiva	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∧ ( 𝐵 ‘ 𝑋 ) = 1o ) → ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ¬ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
130	40 129	mtand	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ¬ ( 𝐵 ‘ 𝑋 ) = 1o )
131		nofv	⊢ ( 𝐵 ∈ No → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) )
132	32 131	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) )
133		3orrot	⊢ ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) ↔ ( ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ∨ ( 𝐵 ‘ 𝑋 ) = ∅ ) )
134		3orrot	⊢ ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ∨ ( 𝐵 ‘ 𝑋 ) = ∅ ) ↔ ( ( 𝐵 ‘ 𝑋 ) = 2o ∨ ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) )
135	133 134	bitri	⊢ ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) ↔ ( ( 𝐵 ‘ 𝑋 ) = 2o ∨ ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) )
136	132 135	sylib	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( ( 𝐵 ‘ 𝑋 ) = 2o ∨ ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) )
137	31 130 136	ecase23d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝐴 <s 𝐵 ) ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) → ( 𝐵 ‘ 𝑋 ) = 2o )