Metamath Proof Explorer

Theorem noinfbnd1lem1

Description: Lemma for noinfbnd1 . Establish a soft lower bound. (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 noinfbnd1lem1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬U↾dom⁡T<sT

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 1 noinfno ⊢B⊆No∧B∈V→T∈No
3 2 3ad2ant2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T∈No
4 simp2l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→B⊆No
5 simp3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈B
6 4 5 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈No
7 nodmon ⊢T∈No→dom⁡T∈On
8 3 7 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→dom⁡T∈On
9 noreson ⊢U∈No∧dom⁡T∈On→U↾dom⁡T∈No
10 6 8 9 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾dom⁡T∈No
11 ssidd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→dom⁡T⊆dom⁡T
12 dmres ⊢dom⁡U↾dom⁡T=dom⁡T∩dom⁡U
13 inss1 ⊢dom⁡T∩dom⁡U⊆dom⁡T
14 12 13 eqsstri ⊢dom⁡U↾dom⁡T⊆dom⁡T
15 14 a1i ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→dom⁡U↾dom⁡T⊆dom⁡T
16 nodmord ⊢T∈No→Ord⁡dom⁡T
17 3 16 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→Ord⁡dom⁡T
18 ordsucss ⊢Ord⁡dom⁡T→h∈dom⁡T→suc⁡h⊆dom⁡T
19 17 18 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→h∈dom⁡T→suc⁡h⊆dom⁡T
20 19 imp ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧h∈dom⁡T→suc⁡h⊆dom⁡T
21 20 resabs1d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧h∈dom⁡T→U↾dom⁡T↾suc⁡h=U↾suc⁡h
22 1 noinfdm ⊢¬∃x∈B∀y∈B¬y<sx→dom⁡T=h|∃p∈Bh∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h
23 22 eleq2d ⊢¬∃x∈B∀y∈B¬y<sx→h∈dom⁡T↔h∈h|∃p∈Bh∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h
24 abid ⊢h∈h|∃p∈Bh∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h↔∃p∈Bh∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h
25 breq2 ⊢q=v→p<sq↔p<sv
26 25 notbid ⊢q=v→¬p<sq↔¬p<sv
27 reseq1 ⊢q=v→q↾suc⁡h=v↾suc⁡h
28 27 eqeq2d ⊢q=v→p↾suc⁡h=q↾suc⁡h↔p↾suc⁡h=v↾suc⁡h
29 26 28 imbi12d ⊢q=v→¬p<sq→p↾suc⁡h=q↾suc⁡h↔¬p<sv→p↾suc⁡h=v↾suc⁡h
30 29 cbvralvw ⊢∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h↔∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
31 30 anbi2i ⊢h∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h↔h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
32 31 rexbii ⊢∃p∈Bh∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h↔∃p∈Bh∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
33 24 32 bitri ⊢h∈h|∃p∈Bh∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡h=q↾suc⁡h↔∃p∈Bh∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
34 23 33 bitrdi ⊢¬∃x∈B∀y∈B¬y<sx→h∈dom⁡T↔∃p∈Bh∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
35 34 3ad2ant1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→h∈dom⁡T↔∃p∈Bh∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
36 simpl2l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→B⊆No
37 simprl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→p∈B
38 36 37 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→p∈No
39 6 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→U∈No
40 sltso ⊢<sOrNo
41 soasym ⊢<sOrNo∧p∈No∧U∈No→p<sU→¬U<sp
42 40 41 mpan ⊢p∈No∧U∈No→p<sU→¬U<sp
43 38 39 42 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→p<sU→¬U<sp
44 nodmon ⊢p∈No→dom⁡p∈On
45 38 44 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→dom⁡p∈On
46 simprrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→h∈dom⁡p
47 onelon ⊢dom⁡p∈On∧h∈dom⁡p→h∈On
48 45 46 47 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→h∈On
49 onsucb ⊢h∈On↔suc⁡h∈On
50 48 49 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→suc⁡h∈On
51 sltres ⊢U∈No∧p∈No∧suc⁡h∈On→U↾suc⁡h<sp↾suc⁡h→U<sp
52 39 38 50 51 syl3anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→U↾suc⁡h<sp↾suc⁡h→U<sp
53 43 52 nsyld ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→p<sU→¬U↾suc⁡h<sp↾suc⁡h
54 noreson ⊢U∈No∧suc⁡h∈On→U↾suc⁡h∈No
55 39 50 54 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→U↾suc⁡h∈No
56 sonr ⊢<sOrNo∧U↾suc⁡h∈No→¬U↾suc⁡h<sU↾suc⁡h
57 40 56 mpan ⊢U↾suc⁡h∈No→¬U↾suc⁡h<sU↾suc⁡h
58 55 57 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬U↾suc⁡h<sU↾suc⁡h
59 58 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h∧¬p<sU→¬U↾suc⁡h<sU↾suc⁡h
60 breq2 ⊢v=U→p<sv↔p<sU
61 60 notbid ⊢v=U→¬p<sv↔¬p<sU
62 reseq1 ⊢v=U→v↾suc⁡h=U↾suc⁡h
63 62 eqeq2d ⊢v=U→p↾suc⁡h=v↾suc⁡h↔p↾suc⁡h=U↾suc⁡h
64 61 63 imbi12d ⊢v=U→¬p<sv→p↾suc⁡h=v↾suc⁡h↔¬p<sU→p↾suc⁡h=U↾suc⁡h
65 simprrr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h
66 simpl3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→U∈B
67 64 65 66 rspcdva ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬p<sU→p↾suc⁡h=U↾suc⁡h
68 67 imp ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h∧¬p<sU→p↾suc⁡h=U↾suc⁡h
69 68 breq2d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h∧¬p<sU→U↾suc⁡h<sp↾suc⁡h↔U↾suc⁡h<sU↾suc⁡h
70 59 69 mtbird ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h∧¬p<sU→¬U↾suc⁡h<sp↾suc⁡h
71 70 ex ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬p<sU→¬U↾suc⁡h<sp↾suc⁡h
72 53 71 pm2.61d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬U↾suc⁡h<sp↾suc⁡h
73 simpl1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬∃x∈B∀y∈B¬y<sx
74 simpl2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→B⊆No∧B∈V
75 1 noinfres ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→T↾suc⁡h=p↾suc⁡h
76 73 74 37 46 65 75 syl113anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→T↾suc⁡h=p↾suc⁡h
77 76 breq2d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→U↾suc⁡h<sT↾suc⁡h↔U↾suc⁡h<sp↾suc⁡h
78 72 77 mtbird ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧p∈B∧h∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬U↾suc⁡h<sT↾suc⁡h
79 78 rexlimdvaa ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃p∈Bh∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡h=v↾suc⁡h→¬U↾suc⁡h<sT↾suc⁡h
80 35 79 sylbid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→h∈dom⁡T→¬U↾suc⁡h<sT↾suc⁡h
81 80 imp ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧h∈dom⁡T→¬U↾suc⁡h<sT↾suc⁡h
82 21 81 eqnbrtrd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧h∈dom⁡T→¬U↾dom⁡T↾suc⁡h<sT↾suc⁡h
83 82 ralrimiva ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∀h∈dom⁡T¬U↾dom⁡T↾suc⁡h<sT↾suc⁡h
84 noresle ⊢T∈No∧U↾dom⁡T∈No∧dom⁡T⊆dom⁡T∧dom⁡U↾dom⁡T⊆dom⁡T∧∀h∈dom⁡T¬U↾dom⁡T↾suc⁡h<sT↾suc⁡h→¬U↾dom⁡T<sT
85 3 10 11 15 83 84 syl23anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬U↾dom⁡T<sT