Metamath Proof Explorer


Theorem noinfbnd1lem2

Description: Lemma for noinfbnd1 . When there is no minimum, if any member of B is a prolongment of T , then so are all elements below it. (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 noinfbnd1lem2 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <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 simp3rl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → 𝑊𝐵 )
3 1 noinfbnd1lem1 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ 𝑊𝐵 ) → ¬ ( 𝑊 ↾ dom 𝑇 ) <s 𝑇 )
4 2 3 syld3an3 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ¬ ( 𝑊 ↾ dom 𝑇 ) <s 𝑇 )
5 simp3rr ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ¬ 𝑈 <s 𝑊 )
6 simp2l ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → 𝐵 No )
7 simp3ll ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → 𝑈𝐵 )
8 6 7 sseldd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → 𝑈 No )
9 6 2 sseldd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → 𝑊 No )
10 1 noinfno ( ( 𝐵 No 𝐵𝑉 ) → 𝑇 No )
11 10 3ad2ant2 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → 𝑇 No )
12 nodmon ( 𝑇 No → dom 𝑇 ∈ On )
13 11 12 syl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → dom 𝑇 ∈ On )
14 sltres ( ( 𝑈 No 𝑊 No ∧ dom 𝑇 ∈ On ) → ( ( 𝑈 ↾ dom 𝑇 ) <s ( 𝑊 ↾ dom 𝑇 ) → 𝑈 <s 𝑊 ) )
15 8 9 13 14 syl3anc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ( ( 𝑈 ↾ dom 𝑇 ) <s ( 𝑊 ↾ dom 𝑇 ) → 𝑈 <s 𝑊 ) )
16 5 15 mtod ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ¬ ( 𝑈 ↾ dom 𝑇 ) <s ( 𝑊 ↾ dom 𝑇 ) )
17 simp3lr ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
18 17 breq1d ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ( ( 𝑈 ↾ dom 𝑇 ) <s ( 𝑊 ↾ dom 𝑇 ) ↔ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) )
19 16 18 mtbid ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) )
20 noreson ( ( 𝑊 No ∧ dom 𝑇 ∈ On ) → ( 𝑊 ↾ dom 𝑇 ) ∈ No )
21 9 13 20 syl2anc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ( 𝑊 ↾ dom 𝑇 ) ∈ No )
22 sltso <s Or No
23 sotrieq2 ( ( <s Or No ∧ ( ( 𝑊 ↾ dom 𝑇 ) ∈ No 𝑇 No ) ) → ( ( 𝑊 ↾ dom 𝑇 ) = 𝑇 ↔ ( ¬ ( 𝑊 ↾ dom 𝑇 ) <s 𝑇 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) ) )
24 22 23 mpan ( ( ( 𝑊 ↾ dom 𝑇 ) ∈ No 𝑇 No ) → ( ( 𝑊 ↾ dom 𝑇 ) = 𝑇 ↔ ( ¬ ( 𝑊 ↾ dom 𝑇 ) <s 𝑇 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) ) )
25 21 11 24 syl2anc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ( ( 𝑊 ↾ dom 𝑇 ) = 𝑇 ↔ ( ¬ ( 𝑊 ↾ dom 𝑇 ) <s 𝑇 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) ) )
26 4 19 25 mpbir2and ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑊𝐵 ∧ ¬ 𝑈 <s 𝑊 ) ) ) → ( 𝑊 ↾ dom 𝑇 ) = 𝑇 )