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 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
noetasuplem.2 Z = S suc bday B dom S × 1 𝑜
Assertion noetasuplem3 A No A V B V X A X < s Z

Proof

Step Hyp Ref Expression
1 noetasuplem.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
2 noetasuplem.2 Z = S suc bday B dom S × 1 𝑜
3 simpl1 A No A V B V X A A No
4 simpl2 A No A V B V X A A V
5 simpr A No A V B V X A X A
6 1 nosupbnd1 A No A V X A X dom S < s S
7 3 4 5 6 syl3anc A No A V B V X A X dom S < s S
8 2 reseq1i Z dom S = S suc bday B dom S × 1 𝑜 dom S
9 resundir S suc bday B dom S × 1 𝑜 dom S = S dom S suc bday B dom S × 1 𝑜 dom S
10 df-res suc bday B dom S × 1 𝑜 dom S = suc bday B dom S × 1 𝑜 dom S × V
11 disjdifr suc bday B dom S dom S =
12 xpdisj1 suc bday B dom S dom S = suc bday B dom S × 1 𝑜 dom S × V =
13 11 12 ax-mp suc bday B dom S × 1 𝑜 dom S × V =
14 10 13 eqtri suc bday B dom S × 1 𝑜 dom S =
15 14 uneq2i S dom S suc bday B dom S × 1 𝑜 dom S = S dom S
16 un0 S dom S = S dom S
17 9 15 16 3eqtri S suc bday B dom S × 1 𝑜 dom S = S dom S
18 8 17 eqtri Z dom S = S dom S
19 1 nosupno A No A V S No
20 3 4 19 syl2anc A No A V B V X A S No
21 nofun S No Fun S
22 20 21 syl A No A V B V X A Fun S
23 funrel Fun S Rel S
24 resdm Rel S S dom S = S
25 22 23 24 3syl A No A V B V X A S dom S = S
26 18 25 syl5eq A No A V B V X A Z dom S = S
27 7 26 breqtrrd A No A V B V X A X dom S < s Z dom S
28 simp1 A No A V B V A No
29 28 sselda A No A V B V X A X No
30 1 2 noetasuplem1 A No A V B V Z No
31 30 adantr A No A V B V X A Z No
32 nodmon S No dom S On
33 20 32 syl A No A V B V X A dom S On
34 sltres X No Z No dom S On X dom S < s Z dom S X < s Z
35 29 31 33 34 syl3anc A No A V B V X A X dom S < s Z dom S X < s Z
36 27 35 mpd A No A V B V X A X < s Z