Metamath Proof Explorer

Theorem noinfbnd2

Description: Bounding law from below for the surreal infimum. Analagous to proposition 4.3 of Lipparini p. 6. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd2.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion noinfbnd2 ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → ( ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 noinfbnd2.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 nfv ⊢ Ⅎ 𝑥 ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )
3 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥
4 nfriota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
5 4 nfdm ⊢ Ⅎ 𝑥 dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
6 nfcv ⊢ Ⅎ 𝑥 1o
7 5 6 nfop ⊢ Ⅎ 𝑥 ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩
8 7 nfsn ⊢ Ⅎ 𝑥 { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ }
9 4 8 nfun ⊢ Ⅎ 𝑥 ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } )
10 nfcv ⊢ Ⅎ 𝑥 { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
11 nfiota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) )
12 10 11 nfmpt ⊢ Ⅎ 𝑥 ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) )
13 3 9 12 nfif ⊢ Ⅎ 𝑥 if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
14 1 13 nfcxfr ⊢ Ⅎ 𝑥 𝑇
15 nfcv ⊢ Ⅎ 𝑥 <s
16 nfcv ⊢ Ⅎ 𝑥 𝑍
17 14 nfdm ⊢ Ⅎ 𝑥 dom 𝑇
18 16 17 nfres ⊢ Ⅎ 𝑥 ( 𝑍 ↾ dom 𝑇 )
19 14 15 18 nfbr ⊢ Ⅎ 𝑥 𝑇 <s ( 𝑍 ↾ dom 𝑇 )
20 19 nfn ⊢ Ⅎ 𝑥 ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 )
21 2 20 nfim ⊢ Ⅎ 𝑥 ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) )
22 noinfbnd2lem1 ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑥 ) )
23 22 3expb ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ¬ ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑥 ) )
24 rspe ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
25 24 adantr ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
26 25 iftrued ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
27 simpl ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) )
28 simprl1 ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → 𝐵 ⊆ No )
29 nominmo ⊢ ( 𝐵 ⊆ No → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
30 28 29 syl ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
31 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) )
32 25 30 31 sylanbrc ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
33 riota1 ⊢ ( ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 ) )
34 32 33 syl ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 ) )
35 27 34 mpbid ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 )
36 35 dmeqd ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) = dom 𝑥 )
37 36 opeq1d ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ = ⟨ dom 𝑥 , 1o ⟩ )
38 37 sneqd ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } = { ⟨ dom 𝑥 , 1o ⟩ } )
39 35 38 uneq12d ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) = ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) )
40 26 39 eqtrd ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) )
41 1 40 syl5eq ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → 𝑇 = ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) )
42 41 dmeqd ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → dom 𝑇 = dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) )
43 1oex ⊢ 1o ∈ V
44 43 dmsnop ⊢ dom { ⟨ dom 𝑥 , 1o ⟩ } = { dom 𝑥 }
45 44 uneq2i ⊢ ( dom 𝑥 ∪ dom { ⟨ dom 𝑥 , 1o ⟩ } ) = ( dom 𝑥 ∪ { dom 𝑥 } )
46 dmun ⊢ dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) = ( dom 𝑥 ∪ dom { ⟨ dom 𝑥 , 1o ⟩ } )
47 df-suc ⊢ suc dom 𝑥 = ( dom 𝑥 ∪ { dom 𝑥 } )
48 45 46 47 3eqtr4ri ⊢ suc dom 𝑥 = dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } )
49 42 48 eqtr4di ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → dom 𝑇 = suc dom 𝑥 )
50 49 reseq2d ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑍 ↾ dom 𝑇 ) = ( 𝑍 ↾ suc dom 𝑥 ) )
51 41 50 breq12d ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ↔ ( 𝑥 ∪ { ⟨ dom 𝑥 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑥 ) ) )
52 23 51 mtbird ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) )
53 52 exp31 ⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ) )
54 21 53 rexlimi ⊢ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) )
55 54 imp ⊢ ( ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) )
56 simprl3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → 𝑍 ∈ No )
57 1 noinfno ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) → 𝑇 ∈ No )
58 57 3adant3 ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → 𝑇 ∈ No )
59 58 ad2antrl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → 𝑇 ∈ No )
60 nodmon ⊢ ( 𝑇 ∈ No → dom 𝑇 ∈ On )
61 59 60 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → dom 𝑇 ∈ On )
62 noreson ⊢ ( ( 𝑍 ∈ No ∧ dom 𝑇 ∈ On ) → ( 𝑍 ↾ dom 𝑇 ) ∈ No )
63 56 61 62 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑍 ↾ dom 𝑇 ) ∈ No )
64 nofun ⊢ ( 𝑇 ∈ No → Fun 𝑇 )
65 funrel ⊢ ( Fun 𝑇 → Rel 𝑇 )
66 58 64 65 3syl ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → Rel 𝑇 )
67 66 ad2antrl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → Rel 𝑇 )
68 resdm ⊢ ( Rel 𝑇 → ( 𝑇 ↾ dom 𝑇 ) = 𝑇 )
69 67 68 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑇 ↾ dom 𝑇 ) = 𝑇 )
70 69 59 eqeltrd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑇 ↾ dom 𝑇 ) ∈ No )
71 resdmss ⊢ dom ( 𝑍 ↾ dom 𝑇 ) ⊆ dom 𝑇
72 71 a1i ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → dom ( 𝑍 ↾ dom 𝑇 ) ⊆ dom 𝑇 )
73 resdmss ⊢ dom ( 𝑇 ↾ dom 𝑇 ) ⊆ dom 𝑇
74 73 a1i ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → dom ( 𝑇 ↾ dom 𝑇 ) ⊆ dom 𝑇 )
75 1 noinfdm ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { 𝑔 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) } )
76 75 abeq2d ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ( 𝑔 ∈ dom 𝑇 ↔ ∃ 𝑝 ∈ 𝐵 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) )
77 76 adantr ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑔 ∈ dom 𝑇 ↔ ∃ 𝑝 ∈ 𝐵 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) )
78 simpll ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
79 simprl1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → 𝐵 ⊆ No )
80 79 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝐵 ⊆ No )
81 simprl2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → 𝐵 ∈ 𝑉 )
82 81 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝐵 ∈ 𝑉 )
83 simprl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑝 ∈ 𝐵 )
84 simprrl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑔 ∈ dom 𝑝 )
85 simprrr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) )
86 breq2 ⊢ ( 𝑞 = 𝑣 → ( 𝑝 <s 𝑞 ↔ 𝑝 <s 𝑣 ) )
87 86 notbid ⊢ ( 𝑞 = 𝑣 → ( ¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣 ) )
88 reseq1 ⊢ ( 𝑞 = 𝑣 → ( 𝑞 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) )
89 88 eqeq2d ⊢ ( 𝑞 = 𝑣 → ( ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ↔ ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) )
90 87 89 imbi12d ⊢ ( 𝑞 = 𝑣 → ( ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ↔ ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) )
91 90 cbvralvw ⊢ ( ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ↔ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) )
92 85 91 sylib ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) )
93 1 noinfres ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ( 𝑇 ↾ suc 𝑔 ) = ( 𝑝 ↾ suc 𝑔 ) )
94 78 80 82 83 84 92 93 syl123anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( 𝑇 ↾ suc 𝑔 ) = ( 𝑝 ↾ suc 𝑔 ) )
95 breq2 ⊢ ( 𝑏 = 𝑝 → ( 𝑍 <s 𝑏 ↔ 𝑍 <s 𝑝 ) )
96 simplrr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )
97 95 96 83 rspcdva ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑍 <s 𝑝 )
98 56 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑍 ∈ No )
99 80 83 sseldd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑝 ∈ No )
100 sltso ⊢ <s Or No
101 soasym ⊢ ( ( <s Or No ∧ ( 𝑍 ∈ No ∧ 𝑝 ∈ No ) ) → ( 𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍 ) )
102 100 101 mpan ⊢ ( ( 𝑍 ∈ No ∧ 𝑝 ∈ No ) → ( 𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍 ) )
103 98 99 102 syl2anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( 𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍 ) )
104 97 103 mpd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ 𝑝 <s 𝑍 )
105 nodmon ⊢ ( 𝑝 ∈ No → dom 𝑝 ∈ On )
106 99 105 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → dom 𝑝 ∈ On )
107 onelon ⊢ ( ( dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝 ) → 𝑔 ∈ On )
108 106 84 107 syl2anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → 𝑔 ∈ On )
109 sucelon ⊢ ( 𝑔 ∈ On ↔ suc 𝑔 ∈ On )
110 108 109 sylib ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → suc 𝑔 ∈ On )
111 sltres ⊢ ( ( 𝑝 ∈ No ∧ 𝑍 ∈ No ∧ suc 𝑔 ∈ On ) → ( ( 𝑝 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) → 𝑝 <s 𝑍 ) )
112 99 98 110 111 syl3anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ( ( 𝑝 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) → 𝑝 <s 𝑍 ) )
113 104 112 mtod ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ ( 𝑝 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) )
114 94 113 eqnbrtrd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) ) ) → ¬ ( 𝑇 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) )
115 114 rexlimdvaa ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( ∃ 𝑝 ∈ 𝐵 ( 𝑔 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑔 ) = ( 𝑞 ↾ suc 𝑔 ) ) ) → ¬ ( 𝑇 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) ) )
116 77 115 sylbid ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑔 ∈ dom 𝑇 → ¬ ( 𝑇 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) ) )
117 116 imp ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ 𝑔 ∈ dom 𝑇 ) → ¬ ( 𝑇 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) )
118 nodmord ⊢ ( 𝑇 ∈ No → Ord dom 𝑇 )
119 ordsucss ⊢ ( Ord dom 𝑇 → ( 𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇 ) )
120 59 118 119 3syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( 𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇 ) )
121 120 imp ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ 𝑔 ∈ dom 𝑇 ) → suc 𝑔 ⊆ dom 𝑇 )
122 121 resabs1d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ 𝑔 ∈ dom 𝑇 ) → ( ( 𝑇 ↾ dom 𝑇 ) ↾ suc 𝑔 ) = ( 𝑇 ↾ suc 𝑔 ) )
123 121 resabs1d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ 𝑔 ∈ dom 𝑇 ) → ( ( 𝑍 ↾ dom 𝑇 ) ↾ suc 𝑔 ) = ( 𝑍 ↾ suc 𝑔 ) )
124 122 123 breq12d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ 𝑔 ∈ dom 𝑇 ) → ( ( ( 𝑇 ↾ dom 𝑇 ) ↾ suc 𝑔 ) <s ( ( 𝑍 ↾ dom 𝑇 ) ↾ suc 𝑔 ) ↔ ( 𝑇 ↾ suc 𝑔 ) <s ( 𝑍 ↾ suc 𝑔 ) ) )
125 117 124 mtbird ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) ∧ 𝑔 ∈ dom 𝑇 ) → ¬ ( ( 𝑇 ↾ dom 𝑇 ) ↾ suc 𝑔 ) <s ( ( 𝑍 ↾ dom 𝑇 ) ↾ suc 𝑔 ) )
126 125 ralrimiva ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ∀ 𝑔 ∈ dom 𝑇 ¬ ( ( 𝑇 ↾ dom 𝑇 ) ↾ suc 𝑔 ) <s ( ( 𝑍 ↾ dom 𝑇 ) ↾ suc 𝑔 ) )
127 noresle ⊢ ( ( ( ( 𝑍 ↾ dom 𝑇 ) ∈ No ∧ ( 𝑇 ↾ dom 𝑇 ) ∈ No ) ∧ ( dom ( 𝑍 ↾ dom 𝑇 ) ⊆ dom 𝑇 ∧ dom ( 𝑇 ↾ dom 𝑇 ) ⊆ dom 𝑇 ∧ ∀ 𝑔 ∈ dom 𝑇 ¬ ( ( 𝑇 ↾ dom 𝑇 ) ↾ suc 𝑔 ) <s ( ( 𝑍 ↾ dom 𝑇 ) ↾ suc 𝑔 ) ) ) → ¬ ( 𝑇 ↾ dom 𝑇 ) <s ( 𝑍 ↾ dom 𝑇 ) )
128 63 70 72 74 126 127 syl23anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ¬ ( 𝑇 ↾ dom 𝑇 ) <s ( 𝑍 ↾ dom 𝑇 ) )
129 69 breq1d ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ( ( 𝑇 ↾ dom 𝑇 ) <s ( 𝑍 ↾ dom 𝑇 ) ↔ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) )
130 128 129 mtbid ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) )
131 55 130 pm2.61ian ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) )
132 simplr ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) )
133 simpll1 ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ⊆ No )
134 simpll2 ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ∈ 𝑉 )
135 simpr ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
136 1 noinfbnd1 ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) → 𝑇 <s ( 𝑏 ↾ dom 𝑇 ) )
137 133 134 135 136 syl3anc ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑇 <s ( 𝑏 ↾ dom 𝑇 ) )
138 simpl3 ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → 𝑍 ∈ No )
139 simpl1 ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → 𝐵 ⊆ No )
140 simpl2 ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → 𝐵 ∈ 𝑉 )
141 139 140 57 syl2anc ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → 𝑇 ∈ No )
142 141 60 syl ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → dom 𝑇 ∈ On )
143 138 142 62 syl2anc ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → ( 𝑍 ↾ dom 𝑇 ) ∈ No )
144 143 adantr ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑍 ↾ dom 𝑇 ) ∈ No )
145 141 adantr ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑇 ∈ No )
146 139 sselda ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ No )
147 142 adantr ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → dom 𝑇 ∈ On )
148 noreson ⊢ ( ( 𝑏 ∈ No ∧ dom 𝑇 ∈ On ) → ( 𝑏 ↾ dom 𝑇 ) ∈ No )
149 146 147 148 syl2anc ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ dom 𝑇 ) ∈ No )
150 sotr2 ⊢ ( ( <s Or No ∧ ( ( 𝑍 ↾ dom 𝑇 ) ∈ No ∧ 𝑇 ∈ No ∧ ( 𝑏 ↾ dom 𝑇 ) ∈ No ) ) → ( ( ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ∧ 𝑇 <s ( 𝑏 ↾ dom 𝑇 ) ) → ( 𝑍 ↾ dom 𝑇 ) <s ( 𝑏 ↾ dom 𝑇 ) ) )
151 100 150 mpan ⊢ ( ( ( 𝑍 ↾ dom 𝑇 ) ∈ No ∧ 𝑇 ∈ No ∧ ( 𝑏 ↾ dom 𝑇 ) ∈ No ) → ( ( ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ∧ 𝑇 <s ( 𝑏 ↾ dom 𝑇 ) ) → ( 𝑍 ↾ dom 𝑇 ) <s ( 𝑏 ↾ dom 𝑇 ) ) )
152 144 145 149 151 syl3anc ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ∧ 𝑇 <s ( 𝑏 ↾ dom 𝑇 ) ) → ( 𝑍 ↾ dom 𝑇 ) <s ( 𝑏 ↾ dom 𝑇 ) ) )
153 132 137 152 mp2and ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑍 ↾ dom 𝑇 ) <s ( 𝑏 ↾ dom 𝑇 ) )
154 simpll3 ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑍 ∈ No )
155 sltres ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑇 ∈ On ) → ( ( 𝑍 ↾ dom 𝑇 ) <s ( 𝑏 ↾ dom 𝑇 ) → 𝑍 <s 𝑏 ) )
156 154 146 147 155 syl3anc ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑍 ↾ dom 𝑇 ) <s ( 𝑏 ↾ dom 𝑇 ) → 𝑍 <s 𝑏 ) )
157 153 156 mpd ⊢ ( ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑍 <s 𝑏 )
158 157 ralrimiva ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )
159 131 158 impbida ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → ( ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s ( 𝑍 ↾ dom 𝑇 ) ) )