Metamath Proof Explorer

Theorem noetainflem3

Description: Lemma for noeta . W bounds B below . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetainflem.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
noetainflem.2 ⊢ 𝑊 = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
Assertion noetainflem3 ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑊 <s 𝑌 )

Proof

Step Hyp Ref Expression
1 noetainflem.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 noetainflem.2 ⊢ 𝑊 = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
3 simpl2 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝐵 ⊆ No )
4 simpl3 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝐵 ∈ V )
5 1 2 noetainflem2 ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( 𝑊 ↾ dom 𝑇 ) = 𝑇 )
6 3 4 5 syl2anc ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝑊 ↾ dom 𝑇 ) = 𝑇 )
7 simpr ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
8 1 noinfbnd1 ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ 𝑌 ∈ 𝐵 ) → 𝑇 <s ( 𝑌 ↾ dom 𝑇 ) )
9 3 4 7 8 syl3anc ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑇 <s ( 𝑌 ↾ dom 𝑇 ) )
10 6 9 eqbrtrd ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝑊 ↾ dom 𝑇 ) <s ( 𝑌 ↾ dom 𝑇 ) )
11 1 2 noetainflem1 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑊 ∈ No )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑊 ∈ No )
13 simp2 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝐵 ⊆ No )
14 13 sselda ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ No )
15 1 noinfno ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑇 ∈ No )
16 3 4 15 syl2anc ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑇 ∈ No )
17 nodmon ⊢ ( 𝑇 ∈ No → dom 𝑇 ∈ On )
18 16 17 syl ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → dom 𝑇 ∈ On )
19 ltsres ⊢ ( ( 𝑊 ∈ No ∧ 𝑌 ∈ No ∧ dom 𝑇 ∈ On ) → ( ( 𝑊 ↾ dom 𝑇 ) <s ( 𝑌 ↾ dom 𝑇 ) → 𝑊 <s 𝑌 ) )
20 12 14 18 19 syl3anc ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑊 ↾ dom 𝑇 ) <s ( 𝑌 ↾ dom 𝑇 ) → 𝑊 <s 𝑌 ) )
21 10 20 mpd ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑌 ∈ 𝐵 ) → 𝑊 <s 𝑌 )