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 ltsres ⊢ ( ( 𝑈 ∈ 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 ltsso ⊢ <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 𝑇 ) = 𝑇 )