Metamath Proof Explorer

Theorem noinfbnd2

Description: Bounding law from below for the surreal infimum. Analagous to proposition 4.3 of Lipparini p. 6. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd2.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 noinfbnd2 ⊢B⊆No∧B∈V∧Z∈No→∀b∈BZ<sb↔¬T<sZ↾dom⁡T

Proof

Step Hyp Ref Expression
1 noinfbnd2.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 nfv ⊢ℲxB⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb
3 nfre1 ⊢Ⅎx∃x∈B∀y∈B¬y<sx
4 nfriota1 ⊢Ⅎ_xιx∈B|∀y∈B¬y<sx
5 4 nfdm ⊢Ⅎ_xdom⁡ιx∈B|∀y∈B¬y<sx
6 nfcv ⊢Ⅎ_x1𝑜
7 5 6 nfop ⊢Ⅎ_xdom⁡ιx∈B|∀y∈B¬y<sx1𝑜
8 7 nfsn ⊢Ⅎ_xdom⁡ιx∈B|∀y∈B¬y<sx1𝑜
9 4 8 nfun ⊢Ⅎ_xιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
10 nfcv ⊢Ⅎ_xy|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y
11 nfiota1 ⊢Ⅎ_xιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
12 10 11 nfmpt ⊢Ⅎ_xg∈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
13 3 9 12 nfif ⊢Ⅎ_xif∃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
14 1 13 nfcxfr ⊢Ⅎ_xT
15 nfcv ⊢Ⅎ_x<s
16 nfcv ⊢Ⅎ_xZ
17 14 nfdm ⊢Ⅎ_xdom⁡T
18 16 17 nfres ⊢Ⅎ_xZ↾dom⁡T
19 14 15 18 nfbr ⊢ℲxT<sZ↾dom⁡T
20 19 nfn ⊢Ⅎx¬T<sZ↾dom⁡T
21 2 20 nfim ⊢ℲxB⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
22 noinfbnd2lem1 ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬x∪dom⁡x1𝑜<sZ↾suc⁡dom⁡x
23 22 3expb ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬x∪dom⁡x1𝑜<sZ↾suc⁡dom⁡x
24 rspe ⊢x∈B∧∀y∈B¬y<sx→∃x∈B∀y∈B¬y<sx
25 24 adantr ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→∃x∈B∀y∈B¬y<sx
26 25 iftrued ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→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=ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
27 simpl ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→x∈B∧∀y∈B¬y<sx
28 simprl1 ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→B⊆No
29 nominmo ⊢B⊆No→∃*x∈B∀y∈B¬y<sx
30 28 29 syl ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→∃*x∈B∀y∈B¬y<sx
31 reu5 ⊢∃!x∈B∀y∈B¬y<sx↔∃x∈B∀y∈B¬y<sx∧∃*x∈B∀y∈B¬y<sx
32 25 30 31 sylanbrc ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→∃!x∈B∀y∈B¬y<sx
33 riota1 ⊢∃!x∈B∀y∈B¬y<sx→x∈B∧∀y∈B¬y<sx↔ιx∈B|∀y∈B¬y<sx=x
34 32 33 syl ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→x∈B∧∀y∈B¬y<sx↔ιx∈B|∀y∈B¬y<sx=x
35 27 34 mpbid ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→ιx∈B|∀y∈B¬y<sx=x
36 35 dmeqd ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡ιx∈B|∀y∈B¬y<sx=dom⁡x
37 36 opeq1d ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡x1𝑜
38 37 sneqd ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡x1𝑜
39 35 38 uneq12d ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=x∪dom⁡x1𝑜
40 26 39 eqtrd ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→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=x∪dom⁡x1𝑜
41 1 40 eqtrid ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→T=x∪dom⁡x1𝑜
42 41 dmeqd ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡T=dom⁡x∪dom⁡x1𝑜
43 1oex ⊢1𝑜∈V
44 43 dmsnop ⊢dom⁡dom⁡x1𝑜=dom⁡x
45 44 uneq2i ⊢dom⁡x∪dom⁡dom⁡x1𝑜=dom⁡x∪dom⁡x
46 dmun ⊢dom⁡x∪dom⁡x1𝑜=dom⁡x∪dom⁡dom⁡x1𝑜
47 df-suc ⊢suc⁡dom⁡x=dom⁡x∪dom⁡x
48 45 46 47 3eqtr4ri ⊢suc⁡dom⁡x=dom⁡x∪dom⁡x1𝑜
49 42 48 eqtr4di ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡T=suc⁡dom⁡x
50 49 reseq2d ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→Z↾dom⁡T=Z↾suc⁡dom⁡x
51 41 50 breq12d ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→T<sZ↾dom⁡T↔x∪dom⁡x1𝑜<sZ↾suc⁡dom⁡x
52 23 51 mtbird ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
53 52 exp31 ⊢x∈B→∀y∈B¬y<sx→B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
54 21 53 rexlimi ⊢∃x∈B∀y∈B¬y<sx→B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
55 54 imp ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
56 simprl3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→Z∈No
57 1 noinfno ⊢B⊆No∧B∈V→T∈No
58 57 3adant3 ⊢B⊆No∧B∈V∧Z∈No→T∈No
59 58 ad2antrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→T∈No
60 nodmon ⊢T∈No→dom⁡T∈On
61 59 60 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡T∈On
62 noreson ⊢Z∈No∧dom⁡T∈On→Z↾dom⁡T∈No
63 56 61 62 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→Z↾dom⁡T∈No
64 nofun ⊢T∈No→Fun⁡T
65 funrel ⊢Fun⁡T→Rel⁡T
66 58 64 65 3syl ⊢B⊆No∧B∈V∧Z∈No→Rel⁡T
67 66 ad2antrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→Rel⁡T
68 resdm ⊢Rel⁡T→T↾dom⁡T=T
69 67 68 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→T↾dom⁡T=T
70 69 59 eqeltrd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→T↾dom⁡T∈No
71 resdmss ⊢dom⁡Z↾dom⁡T⊆dom⁡T
72 71 a1i ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡Z↾dom⁡T⊆dom⁡T
73 resdmss ⊢dom⁡T↾dom⁡T⊆dom⁡T
74 73 a1i ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→dom⁡T↾dom⁡T⊆dom⁡T
75 1 noinfdm ⊢¬∃x∈B∀y∈B¬y<sx→dom⁡T=g|∃p∈Bg∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g
76 75 eqabrd ⊢¬∃x∈B∀y∈B¬y<sx→g∈dom⁡T↔∃p∈Bg∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g
77 76 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→g∈dom⁡T↔∃p∈Bg∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g
78 simpll ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→¬∃x∈B∀y∈B¬y<sx
79 simprl1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→B⊆No
80 79 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→B⊆No
81 simprl2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→B∈V
82 81 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→B∈V
83 simprl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→p∈B
84 simprrl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→g∈dom⁡p
85 simprrr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g
86 breq2 ⊢q=v→p<sq↔p<sv
87 86 notbid ⊢q=v→¬p<sq↔¬p<sv
88 reseq1 ⊢q=v→q↾suc⁡g=v↾suc⁡g
89 88 eqeq2d ⊢q=v→p↾suc⁡g=q↾suc⁡g↔p↾suc⁡g=v↾suc⁡g
90 87 89 imbi12d ⊢q=v→¬p<sq→p↾suc⁡g=q↾suc⁡g↔¬p<sv→p↾suc⁡g=v↾suc⁡g
91 90 cbvralvw ⊢∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g↔∀v∈B¬p<sv→p↾suc⁡g=v↾suc⁡g
92 85 91 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→∀v∈B¬p<sv→p↾suc⁡g=v↾suc⁡g
93 1 noinfres ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧p∈B∧g∈dom⁡p∧∀v∈B¬p<sv→p↾suc⁡g=v↾suc⁡g→T↾suc⁡g=p↾suc⁡g
94 78 80 82 83 84 92 93 syl123anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→T↾suc⁡g=p↾suc⁡g
95 breq2 ⊢b=p→Z<sb↔Z<sp
96 simplrr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→∀b∈BZ<sb
97 95 96 83 rspcdva ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→Z<sp
98 56 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→Z∈No
99 80 83 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→p∈No
100 sltso ⊢<sOrNo
101 soasym ⊢<sOrNo∧Z∈No∧p∈No→Z<sp→¬p<sZ
102 100 101 mpan ⊢Z∈No∧p∈No→Z<sp→¬p<sZ
103 98 99 102 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→Z<sp→¬p<sZ
104 97 103 mpd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→¬p<sZ
105 nodmon ⊢p∈No→dom⁡p∈On
106 99 105 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→dom⁡p∈On
107 onelon ⊢dom⁡p∈On∧g∈dom⁡p→g∈On
108 106 84 107 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→g∈On
109 onsucb ⊢g∈On↔suc⁡g∈On
110 108 109 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→suc⁡g∈On
111 sltres ⊢p∈No∧Z∈No∧suc⁡g∈On→p↾suc⁡g<sZ↾suc⁡g→p<sZ
112 99 98 110 111 syl3anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→p↾suc⁡g<sZ↾suc⁡g→p<sZ
113 104 112 mtod ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→¬p↾suc⁡g<sZ↾suc⁡g
114 94 113 eqnbrtrd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧p∈B∧g∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→¬T↾suc⁡g<sZ↾suc⁡g
115 114 rexlimdvaa ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→∃p∈Bg∈dom⁡p∧∀q∈B¬p<sq→p↾suc⁡g=q↾suc⁡g→¬T↾suc⁡g<sZ↾suc⁡g
116 77 115 sylbid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→g∈dom⁡T→¬T↾suc⁡g<sZ↾suc⁡g
117 116 imp ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧g∈dom⁡T→¬T↾suc⁡g<sZ↾suc⁡g
118 nodmord ⊢T∈No→Ord⁡dom⁡T
119 ordsucss ⊢Ord⁡dom⁡T→g∈dom⁡T→suc⁡g⊆dom⁡T
120 59 118 119 3syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→g∈dom⁡T→suc⁡g⊆dom⁡T
121 120 imp ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧g∈dom⁡T→suc⁡g⊆dom⁡T
122 121 resabs1d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧g∈dom⁡T→T↾dom⁡T↾suc⁡g=T↾suc⁡g
123 121 resabs1d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧g∈dom⁡T→Z↾dom⁡T↾suc⁡g=Z↾suc⁡g
124 122 123 breq12d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧g∈dom⁡T→T↾dom⁡T↾suc⁡g<sZ↾dom⁡T↾suc⁡g↔T↾suc⁡g<sZ↾suc⁡g
125 117 124 mtbird ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb∧g∈dom⁡T→¬T↾dom⁡T↾suc⁡g<sZ↾dom⁡T↾suc⁡g
126 125 ralrimiva ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→∀g∈dom⁡T¬T↾dom⁡T↾suc⁡g<sZ↾dom⁡T↾suc⁡g
127 noresle ⊢Z↾dom⁡T∈No∧T↾dom⁡T∈No∧dom⁡Z↾dom⁡T⊆dom⁡T∧dom⁡T↾dom⁡T⊆dom⁡T∧∀g∈dom⁡T¬T↾dom⁡T↾suc⁡g<sZ↾dom⁡T↾suc⁡g→¬T↾dom⁡T<sZ↾dom⁡T
128 63 70 72 74 126 127 syl23anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T↾dom⁡T<sZ↾dom⁡T
129 69 breq1d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→T↾dom⁡T<sZ↾dom⁡T↔T<sZ↾dom⁡T
130 128 129 mtbid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
131 55 130 pm2.61ian ⊢B⊆No∧B∈V∧Z∈No∧∀b∈BZ<sb→¬T<sZ↾dom⁡T
132 simplr ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→¬T<sZ↾dom⁡T
133 simpll1 ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→B⊆No
134 simpll2 ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→B∈V
135 simpr ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→b∈B
136 1 noinfbnd1 ⊢B⊆No∧B∈V∧b∈B→T<sb↾dom⁡T
137 133 134 135 136 syl3anc ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→T<sb↾dom⁡T
138 simpl3 ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→Z∈No
139 simpl1 ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→B⊆No
140 simpl2 ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→B∈V
141 139 140 57 syl2anc ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→T∈No
142 141 60 syl ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→dom⁡T∈On
143 138 142 62 syl2anc ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→Z↾dom⁡T∈No
144 143 adantr ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→Z↾dom⁡T∈No
145 141 adantr ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→T∈No
146 139 sselda ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→b∈No
147 142 adantr ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→dom⁡T∈On
148 noreson ⊢b∈No∧dom⁡T∈On→b↾dom⁡T∈No
149 146 147 148 syl2anc ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→b↾dom⁡T∈No
150 sotr2 ⊢<sOrNo∧Z↾dom⁡T∈No∧T∈No∧b↾dom⁡T∈No→¬T<sZ↾dom⁡T∧T<sb↾dom⁡T→Z↾dom⁡T<sb↾dom⁡T
151 100 150 mpan ⊢Z↾dom⁡T∈No∧T∈No∧b↾dom⁡T∈No→¬T<sZ↾dom⁡T∧T<sb↾dom⁡T→Z↾dom⁡T<sb↾dom⁡T
152 144 145 149 151 syl3anc ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→¬T<sZ↾dom⁡T∧T<sb↾dom⁡T→Z↾dom⁡T<sb↾dom⁡T
153 132 137 152 mp2and ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→Z↾dom⁡T<sb↾dom⁡T
154 simpll3 ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→Z∈No
155 sltres ⊢Z∈No∧b∈No∧dom⁡T∈On→Z↾dom⁡T<sb↾dom⁡T→Z<sb
156 154 146 147 155 syl3anc ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→Z↾dom⁡T<sb↾dom⁡T→Z<sb
157 153 156 mpd ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T∧b∈B→Z<sb
158 157 ralrimiva ⊢B⊆No∧B∈V∧Z∈No∧¬T<sZ↾dom⁡T→∀b∈BZ<sb
159 131 158 impbida ⊢B⊆No∧B∈V∧Z∈No→∀b∈BZ<sb↔¬T<sZ↾dom⁡T