Metamath Proof Explorer

Theorem tcphex

Description: Lemma for tcphbas and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypothesis tcphex.v 
|- V = ( Base ` W )
Assertion tcphex 
|- ( x e. V |-> ( sqrt ` ( x ., x ) ) ) e. _V

Proof

Step Hyp Ref Expression
1 tcphex.v 
 |-  V = ( Base ` W )
2 eqid 
 |-  ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
3 fvrn0 
 |-  ( sqrt ` ( x ., x ) ) e. ( ran sqrt u. { (/) } )
4 3 a1i 
 |-  ( x e. V -> ( sqrt ` ( x ., x ) ) e. ( ran sqrt u. { (/) } ) )
5 2 4 fmpti 
 |-  ( x e. V |-> ( sqrt ` ( x ., x ) ) ) : V --> ( ran sqrt u. { (/) } )
6 1 fvexi 
 |-  V e. _V
7 cnex 
 |-  CC e. _V
8 sqrtf 
 |-  sqrt : CC --> CC
9 frn 
 |-  ( sqrt : CC --> CC -> ran sqrt C_ CC )
10 8 9 ax-mp 
 |-  ran sqrt C_ CC
11 7 10 ssexi 
 |-  ran sqrt e. _V
12 p0ex 
 |-  { (/) } e. _V
13 11 12 unex 
 |-  ( ran sqrt u. { (/) } ) e. _V
14 fex2 
 |-  ( ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) : V --> ( ran sqrt u. { (/) } ) /\ V e. _V /\ ( ran sqrt u. { (/) } ) e. _V ) -> ( x e. V |-> ( sqrt ` ( x ., x ) ) ) e. _V )
15 5 6 13 14 mp3an 
 |-  ( x e. V |-> ( sqrt ` ( x ., x ) ) ) e. _V