Metamath Proof Explorer


Theorem noinfbnd1lem1

Description: Lemma for noinfbnd1 . Establish a soft lower bound. (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 noinfbnd1lem1 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ¬ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 )

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 𝑇 = if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 1 noinfno ( ( 𝐵 No 𝐵𝑉 ) → 𝑇 No )
3 2 3ad2ant2 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → 𝑇 No )
4 simp2l ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → 𝐵 No )
5 simp3 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → 𝑈𝐵 )
6 4 5 sseldd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → 𝑈 No )
7 nodmon ( 𝑇 No → dom 𝑇 ∈ On )
8 3 7 syl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → dom 𝑇 ∈ On )
9 noreson ( ( 𝑈 No ∧ dom 𝑇 ∈ On ) → ( 𝑈 ↾ dom 𝑇 ) ∈ No )
10 6 8 9 syl2anc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ( 𝑈 ↾ dom 𝑇 ) ∈ No )
11 ssidd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → dom 𝑇 ⊆ dom 𝑇 )
12 dmres dom ( 𝑈 ↾ dom 𝑇 ) = ( dom 𝑇 ∩ dom 𝑈 )
13 inss1 ( dom 𝑇 ∩ dom 𝑈 ) ⊆ dom 𝑇
14 12 13 eqsstri dom ( 𝑈 ↾ dom 𝑇 ) ⊆ dom 𝑇
15 14 a1i ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → dom ( 𝑈 ↾ dom 𝑇 ) ⊆ dom 𝑇 )
16 nodmord ( 𝑇 No → Ord dom 𝑇 )
17 3 16 syl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → Ord dom 𝑇 )
18 ordsucss ( Ord dom 𝑇 → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇 ) )
19 17 18 syl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇 ) )
20 19 imp ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ∈ dom 𝑇 ) → suc ⊆ dom 𝑇 )
21 20 resabs1d ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ∈ dom 𝑇 ) → ( ( 𝑈 ↾ dom 𝑇 ) ↾ suc ) = ( 𝑈 ↾ suc ) )
22 1 noinfdm ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { ∣ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) } )
23 22 eleq2d ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ∈ { ∣ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) } ) )
24 abid ( ∈ { ∣ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) } ↔ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) )
25 breq2 ( 𝑞 = 𝑣 → ( 𝑝 <s 𝑞𝑝 <s 𝑣 ) )
26 25 notbid ( 𝑞 = 𝑣 → ( ¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣 ) )
27 reseq1 ( 𝑞 = 𝑣 → ( 𝑞 ↾ suc ) = ( 𝑣 ↾ suc ) )
28 27 eqeq2d ( 𝑞 = 𝑣 → ( ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ↔ ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) )
29 26 28 imbi12d ( 𝑞 = 𝑣 → ( ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ↔ ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) )
30 29 cbvralvw ( ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ↔ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) )
31 30 anbi2i ( ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) ↔ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) )
32 31 rexbii ( ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) ↔ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) )
33 24 32 bitri ( ∈ { ∣ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑞𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc ) = ( 𝑞 ↾ suc ) ) ) } ↔ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) )
34 23 33 bitrdi ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ↔ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) )
35 34 3ad2ant1 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ( ∈ dom 𝑇 ↔ ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) )
36 simpl2l ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → 𝐵 No )
37 simprl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → 𝑝𝐵 )
38 36 37 sseldd ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → 𝑝 No )
39 6 adantr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → 𝑈 No )
40 sltso <s Or No
41 soasym ( ( <s Or No ∧ ( 𝑝 No 𝑈 No ) ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
42 40 41 mpan ( ( 𝑝 No 𝑈 No ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
43 38 39 42 syl2anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
44 nodmon ( 𝑝 No → dom 𝑝 ∈ On )
45 38 44 syl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → dom 𝑝 ∈ On )
46 simprrl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ∈ dom 𝑝 )
47 onelon ( ( dom 𝑝 ∈ On ∧ ∈ dom 𝑝 ) → ∈ On )
48 45 46 47 syl2anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ∈ On )
49 sucelon ( ∈ On ↔ suc ∈ On )
50 48 49 sylib ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → suc ∈ On )
51 sltres ( ( 𝑈 No 𝑝 No ∧ suc ∈ On ) → ( ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) → 𝑈 <s 𝑝 ) )
52 39 38 50 51 syl3anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) → 𝑈 <s 𝑝 ) )
53 43 52 nsyld ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( 𝑝 <s 𝑈 → ¬ ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) ) )
54 noreson ( ( 𝑈 No ∧ suc ∈ On ) → ( 𝑈 ↾ suc ) ∈ No )
55 39 50 54 syl2anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( 𝑈 ↾ suc ) ∈ No )
56 sonr ( ( <s Or No ∧ ( 𝑈 ↾ suc ) ∈ No ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑈 ↾ suc ) )
57 40 56 mpan ( ( 𝑈 ↾ suc ) ∈ No → ¬ ( 𝑈 ↾ suc ) <s ( 𝑈 ↾ suc ) )
58 55 57 syl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑈 ↾ suc ) )
59 58 adantr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) ∧ ¬ 𝑝 <s 𝑈 ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑈 ↾ suc ) )
60 breq2 ( 𝑣 = 𝑈 → ( 𝑝 <s 𝑣𝑝 <s 𝑈 ) )
61 60 notbid ( 𝑣 = 𝑈 → ( ¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈 ) )
62 reseq1 ( 𝑣 = 𝑈 → ( 𝑣 ↾ suc ) = ( 𝑈 ↾ suc ) )
63 62 eqeq2d ( 𝑣 = 𝑈 → ( ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ↔ ( 𝑝 ↾ suc ) = ( 𝑈 ↾ suc ) ) )
64 61 63 imbi12d ( 𝑣 = 𝑈 → ( ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ↔ ( ¬ 𝑝 <s 𝑈 → ( 𝑝 ↾ suc ) = ( 𝑈 ↾ suc ) ) ) )
65 simprrr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) )
66 simpl3 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → 𝑈𝐵 )
67 64 65 66 rspcdva ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( ¬ 𝑝 <s 𝑈 → ( 𝑝 ↾ suc ) = ( 𝑈 ↾ suc ) ) )
68 67 imp ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) ∧ ¬ 𝑝 <s 𝑈 ) → ( 𝑝 ↾ suc ) = ( 𝑈 ↾ suc ) )
69 68 breq2d ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) ∧ ¬ 𝑝 <s 𝑈 ) → ( ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) ↔ ( 𝑈 ↾ suc ) <s ( 𝑈 ↾ suc ) ) )
70 59 69 mtbird ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) ∧ ¬ 𝑝 <s 𝑈 ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) )
71 70 ex ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( ¬ 𝑝 <s 𝑈 → ¬ ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) ) )
72 53 71 pm2.61d ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) )
73 simpl1 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
74 simpl2 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( 𝐵 No 𝐵𝑉 ) )
75 1 noinfres ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑝𝐵 ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) → ( 𝑇 ↾ suc ) = ( 𝑝 ↾ suc ) )
76 73 74 37 46 65 75 syl113anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( 𝑇 ↾ suc ) = ( 𝑝 ↾ suc ) )
77 76 breq2d ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ( ( 𝑈 ↾ suc ) <s ( 𝑇 ↾ suc ) ↔ ( 𝑈 ↾ suc ) <s ( 𝑝 ↾ suc ) ) )
78 72 77 mtbird ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ( 𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) ) ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑇 ↾ suc ) )
79 78 rexlimdvaa ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ( ∃ 𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀ 𝑣𝐵 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc ) = ( 𝑣 ↾ suc ) ) ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑇 ↾ suc ) ) )
80 35 79 sylbid ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ( ∈ dom 𝑇 → ¬ ( 𝑈 ↾ suc ) <s ( 𝑇 ↾ suc ) ) )
81 80 imp ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ∈ dom 𝑇 ) → ¬ ( 𝑈 ↾ suc ) <s ( 𝑇 ↾ suc ) )
82 21 81 eqnbrtrd ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) ∧ ∈ dom 𝑇 ) → ¬ ( ( 𝑈 ↾ dom 𝑇 ) ↾ suc ) <s ( 𝑇 ↾ suc ) )
83 82 ralrimiva ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ∀ ∈ dom 𝑇 ¬ ( ( 𝑈 ↾ dom 𝑇 ) ↾ suc ) <s ( 𝑇 ↾ suc ) )
84 noresle ( ( ( 𝑇 No ∧ ( 𝑈 ↾ dom 𝑇 ) ∈ No ) ∧ ( dom 𝑇 ⊆ dom 𝑇 ∧ dom ( 𝑈 ↾ dom 𝑇 ) ⊆ dom 𝑇 ∧ ∀ ∈ dom 𝑇 ¬ ( ( 𝑈 ↾ dom 𝑇 ) ↾ suc ) <s ( 𝑇 ↾ suc ) ) ) → ¬ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 )
85 3 10 11 15 83 84 syl23anc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑈𝐵 ) → ¬ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 )