Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj553 Structured version   Unicode version

Theorem bnj553 32204
 Description: Technical lemma for bnj852 32227. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj553.1
bnj553.2
bnj553.3
bnj553.4
bnj553.5
bnj553.6
bnj553.7
bnj553.8
bnj553.9
bnj553.10
bnj553.11
bnj553.12
Assertion
Ref Expression
bnj553
Distinct variable groups:   ,,,   ,   ,,,   ,,,   ,,   ,
Allowed substitution hints:   (,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,)   (,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,)   (,,,,,,)

Proof of Theorem bnj553
StepHypRef Expression
1 bnj553.12 . . . . 5
21bnj930 32076 . . . 4
3 opex 4659 . . . . . . 7
43snid 4008 . . . . . 6
5 elun2 3627 . . . . . 6
64, 5ax-mp 5 . . . . 5
7 bnj553.8 . . . . 5
86, 7eleqtrri 2539 . . . 4
9 funopfv 5835 . . . 4
102, 8, 9mpisyl 18 . . 3
12 fveq2 5794 . . . . . 6
1312bnj1113 32092 . . . . 5
14 bnj553.11 . . . . 5
15 bnj553.10 . . . . 5
1613, 14, 153eqtr4g 2518 . . . 4
18 bnj553.5 . . . . 5
19 bnj553.9 . . . . 5
20 bnj553.4 . . . . 5
2118, 19, 15, 20, 1bnj548 32203 . . . 4