Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2lem3 Structured version   Visualization version   Unicode version

Theorem fpwwe2lem3 9076
 Description: Lemma for fpwwe2 9086. (Contributed by Mario Carneiro, 19-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1
fpwwe2.2
fpwwe2lem4.4
Assertion
Ref Expression
fpwwe2lem3
Distinct variable groups:   ,,   ,,,,   ,,,,   ,,,,   ,,   ,,,,   ,,,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem fpwwe2lem3
StepHypRef Expression
1 fpwwe2lem4.4 . . . . 5
2 fpwwe2.1 . . . . . 6
3 fpwwe2.2 . . . . . 6
42, 3fpwwe2lem2 9075 . . . . 5
51, 4mpbid 215 . . . 4
65simprrd 775 . . 3
7 sneq 3969 . . . . . 6
87imaeq2d 5174 . . . . 5
9 eqeq2 2482 . . . . 5
108, 9sbceqbid 3262 . . . 4
1110rspccva 3135 . . 3
126, 11sylan 479 . 2
13 cnvimass 5194 . . . . 5
142relopabi 4964 . . . . . . 7
1514brrelex2i 4881 . . . . . 6
16 dmexg 6743 . . . . . 6
171, 15, 163syl 18 . . . . 5
18 ssexg 4542 . . . . 5
1913, 17, 18sylancr 676 . . . 4
20 id 22 . . . . . . 7
2120sqxpeqd 4865 . . . . . . . 8
2221ineq2d 3625 . . . . . . 7
2320, 22oveq12d 6326 . . . . . 6
2423eqeq1d 2473 . . . . 5
2524sbcieg 3288 . . . 4
2619, 25syl 17 . . 3