Metamath Proof Explorer


Theorem nosupbnd2

Description: Bounding law from above for the surreal supremum. Proposition 4.3 of Lipparini p. 6. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Hypothesis nosupbnd2.1 𝑆 = if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
Assertion nosupbnd2 ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → ( ∀ 𝑎𝐴 𝑎 <s 𝑍 ↔ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) )

Proof

Step Hyp Ref Expression
1 nosupbnd2.1 𝑆 = if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 nfv 𝑥 ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 )
3 nfcv 𝑥 𝑍
4 nfre1 𝑥𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦
5 nfriota1 𝑥 ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
6 5 nfdm 𝑥 dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
7 nfcv 𝑥 2o
8 6 7 nfop 𝑥 ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o
9 8 nfsn 𝑥 { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ }
10 5 9 nfun 𝑥 ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } )
11 nfcv 𝑥 { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
12 nfiota1 𝑥 ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
13 11 12 nfmpt 𝑥 ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) )
14 4 10 13 nfif 𝑥 if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
15 1 14 nfcxfr 𝑥 𝑆
16 15 nfdm 𝑥 dom 𝑆
17 3 16 nfres 𝑥 ( 𝑍 ↾ dom 𝑆 )
18 nfcv 𝑥 <s
19 17 18 15 nfbr 𝑥 ( 𝑍 ↾ dom 𝑆 ) <s 𝑆
20 19 nfn 𝑥 ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆
21 2 20 nfim 𝑥 ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 )
22 simpl ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) )
23 rspe ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
24 23 adantr ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
25 nomaxmo ( 𝐴 No → ∃* 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
26 25 3ad2ant1 ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → ∃* 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
27 26 ad2antrl ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ∃* 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
28 reu5 ( ∃! 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃* 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) )
29 24 27 28 sylanbrc ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ∃! 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
30 riota1 ( ∃! 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ↔ ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 ) )
31 29 30 syl ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ↔ ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 ) )
32 22 31 mpbid ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 )
33 nosupbnd2lem1 ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ suc dom 𝑥 ) <s ( 𝑥 ∪ { ⟨ dom 𝑥 , 2o ⟩ } ) )
34 33 3expb ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ¬ ( 𝑍 ↾ suc dom 𝑥 ) <s ( 𝑥 ∪ { ⟨ dom 𝑥 , 2o ⟩ } ) )
35 dmeq ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = dom 𝑥 )
36 suceq ( dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = dom 𝑥 → suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = suc dom 𝑥 )
37 35 36 syl ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = suc dom 𝑥 )
38 37 reseq2d ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) = ( 𝑍 ↾ suc dom 𝑥 ) )
39 id ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 )
40 35 opeq1d ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ = ⟨ dom 𝑥 , 2o ⟩ )
41 40 sneqd ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } = { ⟨ dom 𝑥 , 2o ⟩ } )
42 39 41 uneq12d ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = ( 𝑥 ∪ { ⟨ dom 𝑥 , 2o ⟩ } ) )
43 38 42 breq12d ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ( ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) <s ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) ↔ ( 𝑍 ↾ suc dom 𝑥 ) <s ( 𝑥 ∪ { ⟨ dom 𝑥 , 2o ⟩ } ) ) )
44 43 notbid ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ( ¬ ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) <s ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) ↔ ¬ ( 𝑍 ↾ suc dom 𝑥 ) <s ( 𝑥 ∪ { ⟨ dom 𝑥 , 2o ⟩ } ) ) )
45 34 44 syl5ibrcom ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = 𝑥 → ¬ ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) <s ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) ) )
46 32 45 mpd ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ¬ ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) <s ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
47 iftrue ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
48 1 47 syl5eq ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
49 23 48 syl ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) → 𝑆 = ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
50 49 dmeqd ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) → dom 𝑆 = dom ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
51 2on 2o ∈ On
52 51 elexi 2o ∈ V
53 52 dmsnop dom { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } = { dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) }
54 53 uneq2i ( dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ dom { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = ( dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) } )
55 dmun dom ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = ( dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ dom { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } )
56 df-suc suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) = ( dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) } )
57 54 55 56 3eqtr4i dom ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
58 50 57 eqtrdi ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) → dom 𝑆 = suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) )
59 58 reseq2d ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) → ( 𝑍 ↾ dom 𝑆 ) = ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) )
60 59 adantr ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑍 ↾ dom 𝑆 ) = ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) )
61 49 adantr ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → 𝑆 = ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
62 60 61 breq12d ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ↔ ( 𝑍 ↾ suc dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ) <s ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) ) )
63 46 62 mtbird ( ( ( 𝑥𝐴 ∧ ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 )
64 63 exp31 ( 𝑥𝐴 → ( ∀ 𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ) )
65 21 64 rexlimi ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) )
66 65 imp ( ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 )
67 1 nosupno ( ( 𝐴 No 𝐴 ∈ V ) → 𝑆 No )
68 67 3adant3 ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → 𝑆 No )
69 68 ad2antrl ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → 𝑆 No )
70 nodmon ( 𝑆 No → dom 𝑆 ∈ On )
71 69 70 syl ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → dom 𝑆 ∈ On )
72 noreson ( ( 𝑆 No ∧ dom 𝑆 ∈ On ) → ( 𝑆 ↾ dom 𝑆 ) ∈ No )
73 69 71 72 syl2anc ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑆 ↾ dom 𝑆 ) ∈ No )
74 simprl3 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → 𝑍 No )
75 noreson ( ( 𝑍 No ∧ dom 𝑆 ∈ On ) → ( 𝑍 ↾ dom 𝑆 ) ∈ No )
76 74 71 75 syl2anc ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑍 ↾ dom 𝑆 ) ∈ No )
77 dmres dom ( 𝑆 ↾ dom 𝑆 ) = ( dom 𝑆 ∩ dom 𝑆 )
78 inss2 ( dom 𝑆 ∩ dom 𝑆 ) ⊆ dom 𝑆
79 77 78 eqsstri dom ( 𝑆 ↾ dom 𝑆 ) ⊆ dom 𝑆
80 79 a1i ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → dom ( 𝑆 ↾ dom 𝑆 ) ⊆ dom 𝑆 )
81 dmres dom ( 𝑍 ↾ dom 𝑆 ) = ( dom 𝑆 ∩ dom 𝑍 )
82 inss1 ( dom 𝑆 ∩ dom 𝑍 ) ⊆ dom 𝑆
83 81 82 eqsstri dom ( 𝑍 ↾ dom 𝑆 ) ⊆ dom 𝑆
84 83 a1i ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → dom ( 𝑍 ↾ dom 𝑆 ) ⊆ dom 𝑆 )
85 1 nosupdm ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑔 ∣ ∃ 𝑝𝐴 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) } )
86 85 abeq2d ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( 𝑔 ∈ dom 𝑆 ↔ ∃ 𝑝𝐴 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) )
87 86 adantr ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑔 ∈ dom 𝑆 ↔ ∃ 𝑝𝐴 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) )
88 simprl ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑝𝐴 )
89 simplrr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ∀ 𝑎𝐴 𝑎 <s 𝑍 )
90 breq1 ( 𝑎 = 𝑝 → ( 𝑎 <s 𝑍𝑝 <s 𝑍 ) )
91 90 rspcv ( 𝑝𝐴 → ( ∀ 𝑎𝐴 𝑎 <s 𝑍𝑝 <s 𝑍 ) )
92 88 89 91 sylc ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑝 <s 𝑍 )
93 simprl1 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → 𝐴 No )
94 93 adantr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝐴 No )
95 94 88 sseldd ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑝 No )
96 74 adantr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑍 No )
97 sltso <s Or No
98 soasym ( ( <s Or No ∧ ( 𝑝 No 𝑍 No ) ) → ( 𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝 ) )
99 97 98 mpan ( ( 𝑝 No 𝑍 No ) → ( 𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝 ) )
100 95 96 99 syl2anc ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( 𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝 ) )
101 92 100 mpd ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ 𝑍 <s 𝑝 )
102 nodmon ( 𝑝 No → dom 𝑝 ∈ On )
103 95 102 syl ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → dom 𝑝 ∈ On )
104 simprrl ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑔 ∈ dom 𝑝 )
105 onelon ( ( dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝 ) → 𝑔 ∈ On )
106 103 104 105 syl2anc ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑔 ∈ On )
107 sucelon ( 𝑔 ∈ On ↔ suc 𝑔 ∈ On )
108 106 107 sylib ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → suc 𝑔 ∈ On )
109 sltres ( ( 𝑍 No 𝑝 No ∧ suc 𝑔 ∈ On ) → ( ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑝 ↾ suc 𝑔 ) → 𝑍 <s 𝑝 ) )
110 96 95 108 109 syl3anc ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑝 ↾ suc 𝑔 ) → 𝑍 <s 𝑝 ) )
111 101 110 mtod ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑝 ↾ suc 𝑔 ) )
112 simpll ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 )
113 simprl2 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → 𝐴 ∈ V )
114 93 113 jca ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝐴 No 𝐴 ∈ V ) )
115 114 adantr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( 𝐴 No 𝐴 ∈ V ) )
116 simprrr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) )
117 breq1 ( 𝑣 = 𝑞 → ( 𝑣 <s 𝑝𝑞 <s 𝑝 ) )
118 117 notbid ( 𝑣 = 𝑞 → ( ¬ 𝑣 <s 𝑝 ↔ ¬ 𝑞 <s 𝑝 ) )
119 reseq1 ( 𝑣 = 𝑞 → ( 𝑣 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) )
120 119 eqeq2d ( 𝑣 = 𝑞 → ( ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ↔ ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) )
121 118 120 imbi12d ( 𝑣 = 𝑞 → ( ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) )
122 121 cbvralvw ( ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) )
123 116 122 sylibr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) )
124 1 nosupres ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑝𝐴𝑔 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ( 𝑆 ↾ suc 𝑔 ) = ( 𝑝 ↾ suc 𝑔 ) )
125 112 115 88 104 123 124 syl113anc ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( 𝑆 ↾ suc 𝑔 ) = ( 𝑝 ↾ suc 𝑔 ) )
126 125 breq2d ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑆 ↾ suc 𝑔 ) ↔ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑝 ↾ suc 𝑔 ) ) )
127 111 126 mtbird ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑆 ↾ suc 𝑔 ) )
128 127 rexlimdvaa ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( ∃ 𝑝𝐴 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) → ¬ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑆 ↾ suc 𝑔 ) ) )
129 87 128 sylbid ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑔 ∈ dom 𝑆 → ¬ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑆 ↾ suc 𝑔 ) ) )
130 129 imp ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → ¬ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑆 ↾ suc 𝑔 ) )
131 69 adantr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → 𝑆 No )
132 nodmord ( 𝑆 No → Ord dom 𝑆 )
133 131 132 syl ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → Ord dom 𝑆 )
134 simpr ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → 𝑔 ∈ dom 𝑆 )
135 ordsucss ( Ord dom 𝑆 → ( 𝑔 ∈ dom 𝑆 → suc 𝑔 ⊆ dom 𝑆 ) )
136 133 134 135 sylc ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → suc 𝑔 ⊆ dom 𝑆 )
137 136 resabs1d ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) ↾ suc 𝑔 ) = ( 𝑍 ↾ suc 𝑔 ) )
138 136 resabs1d ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → ( ( 𝑆 ↾ dom 𝑆 ) ↾ suc 𝑔 ) = ( 𝑆 ↾ suc 𝑔 ) )
139 137 138 breq12d ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → ( ( ( 𝑍 ↾ dom 𝑆 ) ↾ suc 𝑔 ) <s ( ( 𝑆 ↾ dom 𝑆 ) ↾ suc 𝑔 ) ↔ ( 𝑍 ↾ suc 𝑔 ) <s ( 𝑆 ↾ suc 𝑔 ) ) )
140 130 139 mtbird ( ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) ∧ 𝑔 ∈ dom 𝑆 ) → ¬ ( ( 𝑍 ↾ dom 𝑆 ) ↾ suc 𝑔 ) <s ( ( 𝑆 ↾ dom 𝑆 ) ↾ suc 𝑔 ) )
141 140 ralrimiva ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ∀ 𝑔 ∈ dom 𝑆 ¬ ( ( 𝑍 ↾ dom 𝑆 ) ↾ suc 𝑔 ) <s ( ( 𝑆 ↾ dom 𝑆 ) ↾ suc 𝑔 ) )
142 noresle ( ( ( ( 𝑆 ↾ dom 𝑆 ) ∈ No ∧ ( 𝑍 ↾ dom 𝑆 ) ∈ No ) ∧ ( dom ( 𝑆 ↾ dom 𝑆 ) ⊆ dom 𝑆 ∧ dom ( 𝑍 ↾ dom 𝑆 ) ⊆ dom 𝑆 ∧ ∀ 𝑔 ∈ dom 𝑆 ¬ ( ( 𝑍 ↾ dom 𝑆 ) ↾ suc 𝑔 ) <s ( ( 𝑆 ↾ dom 𝑆 ) ↾ suc 𝑔 ) ) ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑆 ↾ dom 𝑆 ) )
143 73 76 80 84 141 142 syl23anc ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑆 ↾ dom 𝑆 ) )
144 nofun ( 𝑆 No → Fun 𝑆 )
145 69 144 syl ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → Fun 𝑆 )
146 funrel ( Fun 𝑆 → Rel 𝑆 )
147 resdm ( Rel 𝑆 → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
148 145 146 147 3syl ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
149 148 breq2d ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑆 ↾ dom 𝑆 ) ↔ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) )
150 143 149 mtbid ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 )
151 66 150 pm2.61ian ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀ 𝑎𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 )
152 simpll1 ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝐴 No )
153 simpll2 ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝐴 ∈ V )
154 simpr ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝑎𝐴 )
155 1 nosupbnd1 ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑎𝐴 ) → ( 𝑎 ↾ dom 𝑆 ) <s 𝑆 )
156 152 153 154 155 syl3anc ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ( 𝑎 ↾ dom 𝑆 ) <s 𝑆 )
157 simplr ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 )
158 simpl1 ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) → 𝐴 No )
159 158 sselda ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝑎 No )
160 152 153 67 syl2anc ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝑆 No )
161 160 70 syl ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → dom 𝑆 ∈ On )
162 noreson ( ( 𝑎 No ∧ dom 𝑆 ∈ On ) → ( 𝑎 ↾ dom 𝑆 ) ∈ No )
163 159 161 162 syl2anc ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ( 𝑎 ↾ dom 𝑆 ) ∈ No )
164 simpll3 ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝑍 No )
165 164 161 75 syl2anc ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ( 𝑍 ↾ dom 𝑆 ) ∈ No )
166 sotr3 ( ( <s Or No ∧ ( ( 𝑎 ↾ dom 𝑆 ) ∈ No 𝑆 No ∧ ( 𝑍 ↾ dom 𝑆 ) ∈ No ) ) → ( ( ( 𝑎 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) → ( 𝑎 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) ) )
167 97 166 mpan ( ( ( 𝑎 ↾ dom 𝑆 ) ∈ No 𝑆 No ∧ ( 𝑍 ↾ dom 𝑆 ) ∈ No ) → ( ( ( 𝑎 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) → ( 𝑎 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) ) )
168 163 160 165 167 syl3anc ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ( ( ( 𝑎 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) → ( 𝑎 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) ) )
169 156 157 168 mp2and ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ( 𝑎 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) )
170 sltres ( ( 𝑎 No 𝑍 No ∧ dom 𝑆 ∈ On ) → ( ( 𝑎 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) → 𝑎 <s 𝑍 ) )
171 159 164 161 170 syl3anc ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → ( ( 𝑎 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) → 𝑎 <s 𝑍 ) )
172 169 171 mpd ( ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) ∧ 𝑎𝐴 ) → 𝑎 <s 𝑍 )
173 172 ralrimiva ( ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) → ∀ 𝑎𝐴 𝑎 <s 𝑍 )
174 151 173 impbida ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → ( ∀ 𝑎𝐴 𝑎 <s 𝑍 ↔ ¬ ( 𝑍 ↾ dom 𝑆 ) <s 𝑆 ) )