Metamath Proof Explorer

Theorem ltsres

Description: If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011)

Ref Expression
Assertion ltsres ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → 𝐴 <s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 noreson ⊢ ( ( 𝐴 ∈ No ∧ 𝑋 ∈ On ) → ( 𝐴 ↾ 𝑋 ) ∈ No )
2 1 3adant2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( 𝐴 ↾ 𝑋 ) ∈ No )
3 noreson ⊢ ( ( 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( 𝐵 ↾ 𝑋 ) ∈ No )
4 3 3adant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( 𝐵 ↾ 𝑋 ) ∈ No )
5 ltsintdifex ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ∈ No ∧ ( 𝐵 ↾ 𝑋 ) ∈ No ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ V ) )
6 onintrab ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ V ↔ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On )
7 5 6 imbitrdi ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ∈ No ∧ ( 𝐵 ↾ 𝑋 ) ∈ No ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ) )
8 2 4 7 syl2anc ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ) )
9 8 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On )
10 simpl3 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → 𝑋 ∈ On )
11 ltsval2 ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ∈ No ∧ ( 𝐵 ↾ 𝑋 ) ∈ No ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ↔ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) )
12 2 4 11 syl2anc ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ↔ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) )
13 fvex ⊢ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ V
14 fvex ⊢ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ V
15 13 14 brtp ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ↔ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) )
16 1n0 ⊢ 1o ≠ ∅
17 16 neii ⊢ ¬ 1o = ∅
18 eqeq1 ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ↔ 1o = ∅ ) )
19 17 18 mtbiri ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
20 ndmfv ⊢ ( ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
21 19 20 nsyl2 ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) )
22 21 adantr ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) )
23 22 orcd ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
24 21 adantr ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) )
25 24 orcd ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
26 2on ⊢ 2o ∈ On
27 26 elexi ⊢ 2o ∈ V
28 27 prid2 ⊢ 2o ∈ { 1o , 2o }
29 28 nosgnn0i ⊢ ∅ ≠ 2o
30 29 neii ⊢ ¬ ∅ = 2o
31 eqeq1 ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ↔ 2o = ∅ ) )
32 eqcom ⊢ ( 2o = ∅ ↔ ∅ = 2o )
33 31 32 bitrdi ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ↔ ∅ = 2o ) )
34 30 33 mtbiri ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ¬ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
35 ndmfv ⊢ ( ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
36 34 35 nsyl2 ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) )
37 36 adantl ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) )
38 37 olcd ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
39 23 25 38 3jaoi ⊢ ( ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
40 15 39 sylbi ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
41 12 40 biimtrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) ) )
42 41 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
43 dmres ⊢ dom ( 𝐴 ↾ 𝑋 ) = ( 𝑋 ∩ dom 𝐴 )
44 43 elin2 ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ↔ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 ∧ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐴 ) )
45 44 simplbi ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 )
46 dmres ⊢ dom ( 𝐵 ↾ 𝑋 ) = ( 𝑋 ∩ dom 𝐵 )
47 46 elin2 ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ↔ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 ∧ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐵 ) )
48 47 simplbi ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 )
49 45 48 jaoi ⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ∨ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 )
50 42 49 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 )
51 onelss ⊢ ( 𝑋 ∈ On → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ⊆ 𝑋 ) )
52 10 50 51 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ⊆ 𝑋 )
53 52 sselda ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → 𝑦 ∈ 𝑋 )
54 onelon ⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → 𝑦 ∈ On )
55 9 54 sylan ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → 𝑦 ∈ On )
56 intss1 ⊢ ( 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ⊆ 𝑦 )
57 ontri1 ⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ∧ 𝑦 ∈ On ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ⊆ 𝑦 ↔ ¬ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
58 56 57 imbitrid ⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ¬ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
59 58 con2d ⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ¬ 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
60 9 59 sylan ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ¬ 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
61 60 impancom ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( 𝑦 ∈ On → ¬ 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
62 55 61 mpd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ¬ 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } )
63 fveq2 ⊢ ( 𝑎 = 𝑦 → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) = ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) )
64 fveq2 ⊢ ( 𝑎 = 𝑦 → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) )
65 63 64 neeq12d ⊢ ( 𝑎 = 𝑦 → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) ↔ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) ) )
66 65 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ↔ ( 𝑦 ∈ On ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) ) )
67 66 simplbi2 ⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) → 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
68 67 con3d ⊢ ( 𝑦 ∈ On → ( ¬ 𝑦 ∈ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) ) )
69 55 62 68 sylc ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) )
70 df-ne ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) ↔ ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) )
71 70 con2bii ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) ↔ ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) )
72 69 71 sylibr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) )
73 fvres ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
74 fvres ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
75 73 74 eqeq12d ⊢ ( 𝑦 ∈ 𝑋 → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
76 75 biimpd ⊢ ( 𝑦 ∈ 𝑋 → ( ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) → ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
77 53 72 76 sylc ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
78 77 ralrimiva ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
79 fvresval ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∨ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
80 79 ori ⊢ ( ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
81 19 80 nsyl2 ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
82 81 eqcomd ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
83 eqeq2 ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ) )
84 82 83 mpbid ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o )
85 84 adantr ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o )
86 85 a1i ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ) )
87 21 ad2antrl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) )
88 87 45 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 )
89 nofun ⊢ ( ( 𝐵 ↾ 𝑋 ) ∈ No → Fun ( 𝐵 ↾ 𝑋 ) )
90 fvelrn ⊢ ( ( Fun ( 𝐵 ↾ 𝑋 ) ∧ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐵 ↾ 𝑋 ) )
91 90 ex ⊢ ( Fun ( 𝐵 ↾ 𝑋 ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐵 ↾ 𝑋 ) ) )
92 89 91 syl ⊢ ( ( 𝐵 ↾ 𝑋 ) ∈ No → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐵 ↾ 𝑋 ) ) )
93 norn ⊢ ( ( 𝐵 ↾ 𝑋 ) ∈ No → ran ( 𝐵 ↾ 𝑋 ) ⊆ { 1o , 2o } )
94 93 sseld ⊢ ( ( 𝐵 ↾ 𝑋 ) ∈ No → ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐵 ↾ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } ) )
95 92 94 syld ⊢ ( ( 𝐵 ↾ 𝑋 ) ∈ No → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } ) )
96 nosgnn0 ⊢ ¬ ∅ ∈ { 1o , 2o }
97 eleq1 ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } ↔ ∅ ∈ { 1o , 2o } ) )
98 96 97 mtbiri ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ¬ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } )
99 95 98 nsyli ⊢ ( ( 𝐵 ↾ 𝑋 ) ∈ No → ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
100 4 99 syl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
101 100 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) )
102 101 adantrl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) )
103 47 simplbi2 ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐵 → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) ) )
104 103 con3d ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 → ( ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐵 ) )
105 88 102 104 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐵 )
106 ndmfv ⊢ ( ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐵 → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
107 105 106 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ) → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
108 107 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) )
109 86 108 jcad ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ) )
110 fvresval ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∨ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
111 110 ori ⊢ ( ¬ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
112 34 111 nsyl2 ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
113 112 eqcomd ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
114 eqeq2 ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ( ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ↔ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) )
115 113 114 mpbid ⊢ ( ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o )
116 84 115 anim12i ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) )
117 116 a1i ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) )
118 36 ad2antll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐵 ↾ 𝑋 ) )
119 118 48 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 )
120 nofun ⊢ ( ( 𝐴 ↾ 𝑋 ) ∈ No → Fun ( 𝐴 ↾ 𝑋 ) )
121 fvelrn ⊢ ( ( Fun ( 𝐴 ↾ 𝑋 ) ∧ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐴 ↾ 𝑋 ) )
122 121 ex ⊢ ( Fun ( 𝐴 ↾ 𝑋 ) → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐴 ↾ 𝑋 ) ) )
123 120 122 syl ⊢ ( ( 𝐴 ↾ 𝑋 ) ∈ No → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐴 ↾ 𝑋 ) ) )
124 norn ⊢ ( ( 𝐴 ↾ 𝑋 ) ∈ No → ran ( 𝐴 ↾ 𝑋 ) ⊆ { 1o , 2o } )
125 124 sseld ⊢ ( ( 𝐴 ↾ 𝑋 ) ∈ No → ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ ran ( 𝐴 ↾ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } ) )
126 123 125 syld ⊢ ( ( 𝐴 ↾ 𝑋 ) ∈ No → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } ) )
127 eleq1 ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } ↔ ∅ ∈ { 1o , 2o } ) )
128 96 127 mtbiri ⊢ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ¬ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ { 1o , 2o } )
129 126 128 nsyli ⊢ ( ( 𝐴 ↾ 𝑋 ) ∈ No → ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ) )
130 2 129 syl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ) )
131 130 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) )
132 131 adantrr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) )
133 44 simplbi2 ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 → ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐴 → ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) ) )
134 133 con3d ⊢ ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ 𝑋 → ( ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom ( 𝐴 ↾ 𝑋 ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐴 ) )
135 119 132 134 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐴 )
136 135 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐴 ) )
137 ndmfv ⊢ ( ¬ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ dom 𝐴 → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ )
138 136 137 syl6 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) )
139 115 adantl ⊢ ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o )
140 139 a1i ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) )
141 138 140 jcad ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) )
142 109 117 141 3orim123d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ∨ ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) → ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) ) )
143 fvex ⊢ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ V
144 fvex ⊢ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ∈ V
145 143 144 brtp ⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ↔ ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) = 2o ) ) )
146 142 15 145 3imtr4g ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( ( 𝐴 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐵 ↾ 𝑋 ) ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) )
147 12 146 sylbid ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) )
148 147 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
149 raleq ⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
150 fveq2 ⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
151 fveq2 ⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) )
152 150 151 breq12d ⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ( ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) )
153 149 152 anbi12d ⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) ) )
154 153 rspcev ⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ∈ On ∧ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
155 9 78 148 154 syl12anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
156 ltsval ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
157 156 3adant3 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
158 157 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
159 155 158 mpbird ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) ) → 𝐴 <s 𝐵 )
160 159 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) → ( ( 𝐴 ↾ 𝑋 ) <s ( 𝐵 ↾ 𝑋 ) → 𝐴 <s 𝐵 ) )