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 T = if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
Assertion noinfbnd1lem2 ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W W dom T = T

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 T = if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
2 simp3rl ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W W B
3 1 noinfbnd1lem1 ¬ x B y B ¬ y < s x B No B V W B ¬ W dom T < s T
4 2 3 syld3an3 ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W ¬ W dom T < s T
5 simp3rr ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W ¬ U < s W
6 simp2l ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W B No
7 simp3ll ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W U B
8 6 7 sseldd ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W U No
9 6 2 sseldd ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W W No
10 1 noinfno B No B V T No
11 10 3ad2ant2 ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W T No
12 nodmon T No dom T On
13 11 12 syl ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W dom T On
14 sltres U No W No dom T On U dom T < s W dom T U < s W
15 8 9 13 14 syl3anc ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W U dom T < s W dom T U < s W
16 5 15 mtod ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W ¬ U dom T < s W dom T
17 simp3lr ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W U dom T = T
18 17 breq1d ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W U dom T < s W dom T T < s W dom T
19 16 18 mtbid ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W ¬ T < s W dom T
20 noreson W No dom T On W dom T No
21 9 13 20 syl2anc ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W W dom T No
22 sltso < s Or No
23 sotrieq2 < s Or No W dom T No T No W dom T = T ¬ W dom T < s T ¬ T < s W dom T
24 22 23 mpan W dom T No T No W dom T = T ¬ W dom T < s T ¬ T < s W dom T
25 21 11 24 syl2anc ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W W dom T = T ¬ W dom T < s T ¬ T < s W dom T
26 4 19 25 mpbir2and ¬ x B y B ¬ y < s x B No B V U B U dom T = T W B ¬ U < s W W dom T = T