Metamath Proof Explorer


Theorem noetainflem2

Description: Lemma for noeta . The restriction of W to the domain of T is T . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetainflem.1 T=ifxByB¬y<sxιxB|yB¬y<sxdomιxB|yB¬y<sx1𝑜gy|uBydomuvB¬u<svusucy=vsucyιx|uBgdomuvB¬u<svusucg=vsucgug=x
noetainflem.2 W=TsucbdayAdomT×2𝑜
Assertion noetainflem2 BNoBVWdomT=T

Proof

Step Hyp Ref Expression
1 noetainflem.1 T=ifxByB¬y<sxιxB|yB¬y<sxdomιxB|yB¬y<sx1𝑜gy|uBydomuvB¬u<svusucy=vsucyιx|uBgdomuvB¬u<svusucg=vsucgug=x
2 noetainflem.2 W=TsucbdayAdomT×2𝑜
3 2 reseq1i WdomT=TsucbdayAdomT×2𝑜domT
4 resundir TsucbdayAdomT×2𝑜domT=TdomTsucbdayAdomT×2𝑜domT
5 3 4 eqtri WdomT=TdomTsucbdayAdomT×2𝑜domT
6 1 noinfno BNoBVTNo
7 nofun TNoFunT
8 6 7 syl BNoBVFunT
9 funrel FunTRelT
10 resdm RelTTdomT=T
11 8 9 10 3syl BNoBVTdomT=T
12 dmres domsucbdayAdomT×2𝑜domT=domTdomsucbdayAdomT×2𝑜
13 2oex 2𝑜V
14 13 snnz 2𝑜
15 dmxp 2𝑜domsucbdayAdomT×2𝑜=sucbdayAdomT
16 14 15 ax-mp domsucbdayAdomT×2𝑜=sucbdayAdomT
17 16 ineq2i domTdomsucbdayAdomT×2𝑜=domTsucbdayAdomT
18 disjdif domTsucbdayAdomT=
19 17 18 eqtri domTdomsucbdayAdomT×2𝑜=
20 12 19 eqtri domsucbdayAdomT×2𝑜domT=
21 relres RelsucbdayAdomT×2𝑜domT
22 reldm0 RelsucbdayAdomT×2𝑜domTsucbdayAdomT×2𝑜domT=domsucbdayAdomT×2𝑜domT=
23 21 22 ax-mp sucbdayAdomT×2𝑜domT=domsucbdayAdomT×2𝑜domT=
24 20 23 mpbir sucbdayAdomT×2𝑜domT=
25 24 a1i BNoBVsucbdayAdomT×2𝑜domT=
26 11 25 uneq12d BNoBVTdomTsucbdayAdomT×2𝑜domT=T
27 un0 T=T
28 26 27 eqtrdi BNoBVTdomTsucbdayAdomT×2𝑜domT=T
29 5 28 eqtrid BNoBVWdomT=T