Metamath Proof Explorer

Theorem recexpr

Description: The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of Gleason p. 124. (Contributed by NM, 15-May-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion recexpr 
|- ( A e. P. -> E. x e. P. ( A .P. x ) = 1P )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( z = w -> ( z  w
2 1 anbi1d 
 |-  ( z = w -> ( ( z  ( w
3 2 exbidv 
 |-  ( z = w -> ( E. y ( z  E. y ( w
4 3 cbvabv 
 |-  { z | E. y ( z
5 4 reclem2pr 
 |-  ( A e. P. -> { z | E. y ( z
6 4 reclem4pr 
 |-  ( A e. P. -> ( A .P. { z | E. y ( z
7 oveq2 
 |-  ( x = { z | E. y ( z  ( A .P. x ) = ( A .P. { z | E. y ( z
8 7 eqeq1d 
 |-  ( x = { z | E. y ( z  ( ( A .P. x ) = 1P <-> ( A .P. { z | E. y ( z
9 8 rspcev 
 |-  ( ( { z | E. y ( z  E. x e. P. ( A .P. x ) = 1P )
10 5 6 9 syl2anc 
 |-  ( A e. P. -> E. x e. P. ( A .P. x ) = 1P )