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

Theorem sbthlem8 7216
 Description: Lemma for sbth 7219. (Contributed by NM, 27-Mar-1998.)
Hypotheses
Ref Expression
sbthlem.1
sbthlem.2
sbthlem.3
Assertion
Ref Expression
sbthlem8
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem sbthlem8
StepHypRef Expression
1 funres11 5513 . . . 4
2 funcnvcnv 5501 . . . . . 6
3 funres11 5513 . . . . . 6
42, 3syl 16 . . . . 5
54ad3antrrr 711 . . . 4
61, 5anim12i 550 . . 3
7 df-ima 4883 . . . . . . . 8
8 df-rn 4881 . . . . . . . 8
97, 8eqtr2i 2456 . . . . . . 7
10 df-ima 4883 . . . . . . . . 9
11 df-rn 4881 . . . . . . . . 9
1210, 11eqtri 2455 . . . . . . . 8
13 sbthlem.1 . . . . . . . . 9
14 sbthlem.2 . . . . . . . . 9
1513, 14sbthlem4 7212 . . . . . . . 8
1612, 15syl5eqr 2481 . . . . . . 7
17 ineq12 3529 . . . . . . 7
189, 16, 17sylancr 645 . . . . . 6
19 disjdif 3692 . . . . . 6
2018, 19syl6eq 2483 . . . . 5
2120adantlll 699 . . . 4