Metamath Proof Explorer


Theorem opsrtoslem1

Description: Lemma for opsrtos . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrso.o O=IordPwSerRT
opsrso.i φIV
opsrso.r φRToset
opsrso.t φTI×I
opsrso.w φTWeI
opsrtoslem.s S=ImPwSerR
opsrtoslem.b B=BaseS
opsrtoslem.q <˙=<R
opsrtoslem.c C=T<bagI
opsrtoslem.d D=h0I|h-1Fin
opsrtoslem.ps ψzDxz<˙yzwDwCzxw=yw
opsrtoslem.l ˙=O
Assertion opsrtoslem1 φ˙=xy|ψB×BIB

Proof

Step Hyp Ref Expression
1 opsrso.o O=IordPwSerRT
2 opsrso.i φIV
3 opsrso.r φRToset
4 opsrso.t φTI×I
5 opsrso.w φTWeI
6 opsrtoslem.s S=ImPwSerR
7 opsrtoslem.b B=BaseS
8 opsrtoslem.q <˙=<R
9 opsrtoslem.c C=T<bagI
10 opsrtoslem.d D=h0I|h-1Fin
11 opsrtoslem.ps ψzDxz<˙yzwDwCzxw=yw
12 opsrtoslem.l ˙=O
13 6 1 7 8 9 10 12 4 opsrle φ˙=xy|xyBzDxz<˙yzwDwCzxw=ywx=y
14 unopab xy|xyBψxy|xyBx=y=xy|xyBψxyBx=y
15 inopab xy|ψxy|xByB=xy|ψxByB
16 df-xp B×B=xy|xByB
17 16 ineq2i xy|ψB×B=xy|ψxy|xByB
18 vex xV
19 vex yV
20 18 19 prss xByBxyB
21 20 anbi1i xByBψxyBψ
22 ancom xByBψψxByB
23 21 22 bitr3i xyBψψxByB
24 23 opabbii xy|xyBψ=xy|ψxByB
25 15 17 24 3eqtr4i xy|ψB×B=xy|xyBψ
26 opabresid IB=xy|xBy=x
27 equcom x=yy=x
28 27 anbi2i xBx=yxBy=x
29 eleq1w x=yxByB
30 29 biimpac xBx=yyB
31 30 pm4.71i xBx=yxBx=yyB
32 28 31 bitr3i xBy=xxBx=yyB
33 an32 xBx=yyBxByBx=y
34 20 anbi1i xByBx=yxyBx=y
35 32 33 34 3bitri xBy=xxyBx=y
36 35 opabbii xy|xBy=x=xy|xyBx=y
37 26 36 eqtri IB=xy|xyBx=y
38 25 37 uneq12i xy|ψB×BIB=xy|xyBψxy|xyBx=y
39 11 orbi1i ψx=yzDxz<˙yzwDwCzxw=ywx=y
40 39 anbi2i xyBψx=yxyBzDxz<˙yzwDwCzxw=ywx=y
41 andi xyBψx=yxyBψxyBx=y
42 40 41 bitr3i xyBzDxz<˙yzwDwCzxw=ywx=yxyBψxyBx=y
43 42 opabbii xy|xyBzDxz<˙yzwDwCzxw=ywx=y=xy|xyBψxyBx=y
44 14 38 43 3eqtr4ri xy|xyBzDxz<˙yzwDwCzxw=ywx=y=xy|ψB×BIB
45 13 44 eqtrdi φ˙=xy|ψB×BIB