Metamath Proof Explorer

Theorem noetasuplem3

Description: Lemma for noeta . Z is an upper bound for A . Part of Theorem 5.1 of Lipparini p. 7-8. (Contributed by Scott Fenton, 4-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 noetasuplem.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 noetasuplem.2 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
3 simpl1 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ⊆ No )
4 simpl2 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ∈ V )
5 simpr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
6 1 nosupbnd1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ↾ dom 𝑆 ) <s 𝑆 )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ↾ dom 𝑆 ) <s 𝑆 )
8 2 reseq1i ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 )
9 resundir ⊢ ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) )
10 df-res ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) )
11 incom ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
12 disjdif ⊢ ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅
13 11 12 eqtri ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅
14 xpdisj1 ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅ → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅ )
15 13 14 ax-mp ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅
16 10 15 eqtri ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅
17 16 uneq2i ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ )
18 un0 ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ ) = ( 𝑆 ↾ dom 𝑆 )
19 9 17 18 3eqtri ⊢ ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 ) = ( 𝑆 ↾ dom 𝑆 )
20 8 19 eqtri ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( 𝑆 ↾ dom 𝑆 )
21 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
22 3 4 21 syl2anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑆 ∈ No )
23 nofun ⊢ ( 𝑆 ∈ No → Fun 𝑆 )
24 22 23 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → Fun 𝑆 )
25 funrel ⊢ ( Fun 𝑆 → Rel 𝑆 )
26 resdm ⊢ ( Rel 𝑆 → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
27 24 25 26 3syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
28 20 27 syl5eq ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )
29 7 28 breqtrrd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) )
30 simp1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ⊆ No )
31 30 sselda ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ No )
32 1 2 noetasuplem1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑍 ∈ No )
33 32 adantr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑍 ∈ No )
34 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
35 22 34 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → dom 𝑆 ∈ On )
36 sltres ⊢ ( ( 𝑋 ∈ No ∧ 𝑍 ∈ No ∧ dom 𝑆 ∈ On ) → ( ( 𝑋 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) → 𝑋 <s 𝑍 ) )
37 31 33 35 36 syl3anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑋 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) → 𝑋 <s 𝑍 ) )
38 29 37 mpd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 <s 𝑍 )