Metamath Proof Explorer


Theorem sltres

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 sltres ( ( 𝐴 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 sltintdifex ( ( ( 𝐴𝑋 ) ∈ No ∧ ( 𝐵𝑋 ) ∈ No ) → ( ( 𝐴𝑋 ) <s ( 𝐵𝑋 ) → { 𝑎 ∈ On ∣ ( ( 𝐴𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵𝑋 ) ‘ 𝑎 ) } ∈ V ) )
6 onintrab ( { 𝑎 ∈ On ∣ ( ( 𝐴𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵𝑋 ) ‘ 𝑎 ) } ∈ V ↔ { 𝑎 ∈ On ∣ ( ( 𝐴𝑋 ) ‘ 𝑎 ) ≠ ( ( 𝐵𝑋 ) ‘ 𝑎 ) } ∈ On )
7 5 6 syl6ib ( ( ( 𝐴𝑋 ) ∈ 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 sltval2 ( ( ( 𝐴𝑋 ) ∈ 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 syl6bi ( ( 𝐴 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 syl5ib ( ( { 𝑎 ∈ 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 sltval ( ( 𝐴 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 𝐵 ) )