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 disjdifr ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅
12 xpdisj1 ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅ → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅ )
13 11 12 ax-mp ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅
14 10 13 eqtri ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅
15 14 uneq2i ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ )
16 un0 ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ ) = ( 𝑆 ↾ dom 𝑆 )
17 9 15 16 3eqtri ⊢ ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 ) = ( 𝑆 ↾ dom 𝑆 )
18 8 17 eqtri ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( 𝑆 ↾ dom 𝑆 )
19 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
20 3 4 19 syl2anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑆 ∈ No )
21 nofun ⊢ ( 𝑆 ∈ No → Fun 𝑆 )
22 20 21 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → Fun 𝑆 )
23 funrel ⊢ ( Fun 𝑆 → Rel 𝑆 )
24 resdm ⊢ ( Rel 𝑆 → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
25 22 23 24 3syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
26 18 25 syl5eq ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )
27 7 26 breqtrrd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) )
28 simp1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ⊆ No )
29 28 sselda ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ No )
30 1 2 noetasuplem1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑍 ∈ No )
31 30 adantr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑍 ∈ No )
32 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
33 20 32 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → dom 𝑆 ∈ On )
34 sltres ⊢ ( ( 𝑋 ∈ No ∧ 𝑍 ∈ No ∧ dom 𝑆 ∈ On ) → ( ( 𝑋 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) → 𝑋 <s 𝑍 ) )
35 29 31 33 34 syl3anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑋 ↾ dom 𝑆 ) <s ( 𝑍 ↾ dom 𝑆 ) → 𝑋 <s 𝑍 ) )
36 27 35 mpd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 <s 𝑍 )