Metamath Proof Explorer


Theorem noinfbnd1

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

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

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 𝑇 = if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 simpr1 ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝐵 No )
3 simpl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
4 nominmo ( 𝐵 No → ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
5 2 4 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
6 reu5 ( ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
7 3 5 6 sylanbrc ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
8 riotacl ( ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ 𝐵 )
9 7 8 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ 𝐵 )
10 2 9 sseldd ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No )
11 noextendlt ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
12 10 11 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
13 simpr3 ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝑈𝐵 )
14 nfv 𝑥 ( 𝐵 No 𝐵𝑉𝑈𝐵 )
15 nfcv 𝑥 𝐵
16 nfcv 𝑥 𝑦
17 nfcv 𝑥 <s
18 nfriota1 𝑥 ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
19 16 17 18 nfbr 𝑥 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
20 19 nfn 𝑥 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
21 15 20 nfralw 𝑥𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
22 14 21 nfim 𝑥 ( ( 𝐵 No 𝐵𝑉𝑈𝐵 ) → ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
23 simpl ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
24 rspe ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
25 24 adantr ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
26 simpr1 ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝐵 No )
27 26 4 syl ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
28 25 27 6 sylanbrc ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
29 riota1 ( ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 ) )
30 28 29 syl ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 ) )
31 23 30 mpbid ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 )
32 simplr ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 )
33 nfra1 𝑦𝑦𝐵 ¬ 𝑦 <s 𝑥
34 nfcv 𝑦 𝐵
35 33 34 nfriota 𝑦 ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
36 35 nfeq1 𝑦 ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥
37 breq2 ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 → ( 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ 𝑦 <s 𝑥 ) )
38 37 notbid ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 → ( ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ¬ 𝑦 <s 𝑥 ) )
39 36 38 ralbid ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 → ( ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
40 39 biimprd ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = 𝑥 → ( ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 → ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
41 31 32 40 sylc ( ( ( 𝑥𝐵 ∧ ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
42 41 exp31 ( 𝑥𝐵 → ( ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ( 𝐵 No 𝐵𝑉𝑈𝐵 ) → ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ) )
43 22 42 rexlimi ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ( 𝐵 No 𝐵𝑉𝑈𝐵 ) → ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
44 43 imp ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
45 nfcv 𝑦 𝑈
46 nfcv 𝑦 <s
47 45 46 35 nfbr 𝑦 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
48 47 nfn 𝑦 ¬ 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
49 breq1 ( 𝑦 = 𝑈 → ( 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
50 49 notbid ( 𝑦 = 𝑈 → ( ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↔ ¬ 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
51 48 50 rspc ( 𝑈𝐵 → ( ∀ 𝑦𝐵 ¬ 𝑦 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) → ¬ 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
52 13 44 51 sylc ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ¬ 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
53 nofun ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No → Fun ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
54 funrel ( Fun ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) → Rel ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
55 10 53 54 3syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → Rel ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
56 sssucid dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ⊆ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
57 relssres ( ( Rel ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ⊆ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) = ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
58 55 56 57 sylancl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) = ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
59 58 breq2d ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ↔ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
60 2 13 sseldd ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝑈 No )
61 nodmon ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No → dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On )
62 10 61 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On )
63 sucelon ( dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On ↔ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On )
64 62 63 sylib ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On )
65 sltres ( ( 𝑈 No ∧ ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No ∧ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On ) → ( ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) → 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
66 60 10 64 65 syl3anc ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) → 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
67 59 66 sylbird ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) → 𝑈 <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
68 52 67 mtod ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ¬ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
69 1oex 1o ∈ V
70 69 prid1 1o ∈ { 1o , 2o }
71 70 noextend ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) ∈ No )
72 10 71 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) ∈ No )
73 noreson ( ( 𝑈 No ∧ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ On ) → ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ∈ No )
74 60 64 73 syl2anc ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ∈ No )
75 sltso <s Or No
76 sotr3 ( ( <s Or No ∧ ( ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) ∈ No ∧ ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No ∧ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ∈ No ) ) → ( ( ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ¬ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ) )
77 75 76 mpan ( ( ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) ∈ No ∧ ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No ∧ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ∈ No ) → ( ( ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ¬ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ) )
78 72 10 74 77 syl3anc ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∧ ¬ ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) <s ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) ) )
79 12 68 78 mp2and ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) <s ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
80 iftrue ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
81 1 80 syl5eq ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
82 81 adantr ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝑇 = ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
83 81 dmeqd ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
84 69 dmsnop dom { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } = { dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) }
85 84 uneq2i ( dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ dom { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) = ( dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) } )
86 dmun dom ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) = ( dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ dom { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } )
87 df-suc suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) = ( dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) } )
88 85 86 87 3eqtr4i dom ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) = suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
89 83 88 eqtrdi ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
90 89 reseq2d ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( 𝑈 ↾ dom 𝑇 ) = ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
91 90 adantr ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ( 𝑈 ↾ dom 𝑇 ) = ( 𝑈 ↾ suc dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ) )
92 79 82 91 3brtr4d ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) )
93 simpl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
94 simpr1 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝐵 No )
95 simpr2 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝐵𝑉 )
96 simpr3 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝑈𝐵 )
97 1 noinfbnd1lem6 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) )
98 93 94 95 96 97 syl121anc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉𝑈𝐵 ) ) → 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) )
99 92 98 pm2.61ian ( ( 𝐵 No 𝐵𝑉𝑈𝐵 ) → 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) )