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