Metamath Proof Explorer

Theorem noinfbnd1lem4

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not undefined. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd1.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
Assertion noinfbnd1lem4 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U⁡dom⁡T≠∅

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
2 simpl1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→¬∃x∈B∀y∈B¬y<sx
3 simpl2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→B⊆No∧B∈V
4 simprl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→w∈B
5 simpl3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→U∈B∧U↾dom⁡T=T
6 simp2l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→B⊆No
7 6 sselda ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B→w∈No
8 simp3l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U∈B
9 6 8 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U∈No
10 9 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B→U∈No
11 sltso ⊢<sOrNo
12 soasym ⊢<sOrNo∧w∈No∧U∈No→w<sU→¬U<sw
13 11 12 mpan ⊢w∈No∧U∈No→w<sU→¬U<sw
14 7 10 13 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B→w<sU→¬U<sw
15 14 impr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→¬U<sw
16 4 15 jca ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→w∈B∧¬U<sw
17 1 noinfbnd1lem2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧¬U<sw→w↾dom⁡T=T
18 2 3 5 16 17 syl112anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→w↾dom⁡T=T
19 1 noinfbnd1lem3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧w∈B∧w↾dom⁡T=T→w⁡dom⁡T≠1𝑜
20 2 3 4 18 19 syl112anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→w⁡dom⁡T≠1𝑜
21 20 neneqd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B∧w<sU→¬w⁡dom⁡T=1𝑜
22 21 expr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B→w<sU→¬w⁡dom⁡T=1𝑜
23 imnan ⊢w<sU→¬w⁡dom⁡T=1𝑜↔¬w<sU∧w⁡dom⁡T=1𝑜
24 22 23 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧w∈B→¬w<sU∧w⁡dom⁡T=1𝑜
25 24 nrexdv ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→¬∃w∈Bw<sU∧w⁡dom⁡T=1𝑜
26 breq2 ⊢x=U→y<sx↔y<sU
27 26 rexbidv ⊢x=U→∃y∈By<sx↔∃y∈By<sU
28 simpl1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→¬∃x∈B∀y∈B¬y<sx
29 dfral2 ⊢∀x∈B∃y∈By<sx↔¬∃x∈B¬∃y∈By<sx
30 ralnex ⊢∀y∈B¬y<sx↔¬∃y∈By<sx
31 30 rexbii ⊢∃x∈B∀y∈B¬y<sx↔∃x∈B¬∃y∈By<sx
32 29 31 xchbinxr ⊢∀x∈B∃y∈By<sx↔¬∃x∈B∀y∈B¬y<sx
33 28 32 sylibr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→∀x∈B∃y∈By<sx
34 simpl3l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→U∈B
35 27 33 34 rspcdva ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→∃y∈By<sU
36 breq1 ⊢y=w→y<sU↔w<sU
37 36 cbvrexvw ⊢∃y∈By<sU↔∃w∈Bw<sU
38 35 37 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→∃w∈Bw<sU
39 simpl2l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→B⊆No
40 39 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→B⊆No
41 simprl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w∈B
42 40 41 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w∈No
43 34 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→U∈B
44 40 43 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→U∈No
45 simpl2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→B⊆No∧B∈V
46 1 noinfno ⊢B⊆No∧B∈V→T∈No
47 45 46 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→T∈No
48 47 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→T∈No
49 nodmon ⊢T∈No→dom⁡T∈On
50 48 49 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→dom⁡T∈On
51 simpll1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→¬∃x∈B∀y∈B¬y<sx
52 simpll2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→B⊆No∧B∈V
53 simpll3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→U∈B∧U↾dom⁡T=T
54 simprr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w<sU
55 42 44 13 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w<sU→¬U<sw
56 54 55 mpd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→¬U<sw
57 41 56 jca ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w∈B∧¬U<sw
58 51 52 53 57 17 syl112anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w↾dom⁡T=T
59 simpl3r ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→U↾dom⁡T=T
60 59 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→U↾dom⁡T=T
61 58 60 eqtr4d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w↾dom⁡T=U↾dom⁡T
62 simplr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→U⁡dom⁡T=∅
63 nogt01o ⊢w∈No∧U∈No∧dom⁡T∈On∧w↾dom⁡T=U↾dom⁡T∧w<sU∧U⁡dom⁡T=∅→w⁡dom⁡T=1𝑜
64 42 44 50 61 54 62 63 syl321anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B∧w<sU→w⁡dom⁡T=1𝑜
65 64 expr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B→w<sU→w⁡dom⁡T=1𝑜
66 65 ancld ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅∧w∈B→w<sU→w<sU∧w⁡dom⁡T=1𝑜
67 66 reximdva ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→∃w∈Bw<sU→∃w∈Bw<sU∧w⁡dom⁡T=1𝑜
68 38 67 mpd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T∧U⁡dom⁡T=∅→∃w∈Bw<sU∧w⁡dom⁡T=1𝑜
69 25 68 mtand ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→¬U⁡dom⁡T=∅
70 69 neqned ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U⁡dom⁡T≠∅