This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcphex

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

Ref Expression
Hypothesis tcphex.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion tcphex ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ∈ V

Proof

Step Hyp Ref Expression
1 tcphex.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) )
3 fvrn0 ⊢ ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ ( ran √ ∪ { ∅ } )
4 3 a1i ⊢ ( 𝑥 ∈ 𝑉 → ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ ( ran √ ∪ { ∅ } ) )
5 2 4 fmpti ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) : 𝑉 ⟶ ( ran √ ∪ { ∅ } )
6 1 fvexi ⊢ 𝑉 ∈ V
7 cnex ⊢ ℂ ∈ V
8 sqrtf ⊢ √ : ℂ ⟶ ℂ
9 frn ⊢ ( √ : ℂ ⟶ ℂ → ran √ ⊆ ℂ )
10 8 9 ax-mp ⊢ ran √ ⊆ ℂ
11 7 10 ssexi ⊢ ran √ ∈ V
12 p0ex ⊢ { ∅ } ∈ V
13 11 12 unex ⊢ ( ran √ ∪ { ∅ } ) ∈ V
14 fex2 ⊢ ( ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) : 𝑉 ⟶ ( ran √ ∪ { ∅ } ) ∧ 𝑉 ∈ V ∧ ( ran √ ∪ { ∅ } ) ∈ V ) → ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ∈ V )
15 5 6 13 14 mp3an ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ∈ V