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 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 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 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 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 𝐡 ) )