Metamath Proof Explorer


Theorem cvmlift2lem1

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Assertion cvmlift2lem1 y 0 1 u nei II y u × x M u × t M 0 1 × x M 0 1 × t M

Proof

Step Hyp Ref Expression
1 biimp u × x M u × t M u × x M u × t M
2 iitop II Top
3 iiuni 0 1 = II
4 3 neii1 II Top u nei II y u 0 1
5 2 4 mpan u nei II y u 0 1
6 5 adantl 0 1 × x M u nei II y u 0 1
7 xpss1 u 0 1 u × x 0 1 × x
8 6 7 syl 0 1 × x M u nei II y u × x 0 1 × x
9 simpl 0 1 × x M u nei II y 0 1 × x M
10 8 9 sstrd 0 1 × x M u nei II y u × x M
11 ssnei II Top u nei II y y u
12 2 11 mpan u nei II y y u
13 12 adantl 0 1 × x M u nei II y y u
14 vex y V
15 14 snss y u y u
16 13 15 sylibr 0 1 × x M u nei II y y u
17 vsnid t t
18 opelxpi y u t t y t u × t
19 16 17 18 sylancl 0 1 × x M u nei II y y t u × t
20 ssel u × t M y t u × t y t M
21 19 20 syl5com 0 1 × x M u nei II y u × t M y t M
22 10 21 embantd 0 1 × x M u nei II y u × x M u × t M y t M
23 1 22 syl5 0 1 × x M u nei II y u × x M u × t M y t M
24 23 rexlimdva 0 1 × x M u nei II y u × x M u × t M y t M
25 24 ralimdv 0 1 × x M y 0 1 u nei II y u × x M u × t M y 0 1 y t M
26 25 com12 y 0 1 u nei II y u × x M u × t M 0 1 × x M y 0 1 y t M
27 dfss3 0 1 × t M z 0 1 × t z M
28 eleq1 z = y u z M y u M
29 28 ralxp z 0 1 × t z M y 0 1 u t y u M
30 vex t V
31 opeq2 u = t y u = y t
32 31 eleq1d u = t y u M y t M
33 30 32 ralsn u t y u M y t M
34 33 ralbii y 0 1 u t y u M y 0 1 y t M
35 27 29 34 3bitri 0 1 × t M y 0 1 y t M
36 26 35 syl6ibr y 0 1 u nei II y u × x M u × t M 0 1 × x M 0 1 × t M