Theorem tcphex

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

	Ref	Expression
Hypothesis	tcphex.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	tcphex	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		tcphex.v	$$⊢V={\mathrm{Base}}_W$$
2		eqid	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
3		fvrn0	$$⊢\sqrt{x\underset{\dot{}}{,}x}\in \left(\mathrm{ran}\surd \cup \left\{\varnothing \right\}\right)$$
4	3	a1i	$$⊢x\in V\to \sqrt{x\underset{\dot{}}{,}x}\in \left(\mathrm{ran}\surd \cup \left\{\varnothing \right\}\right)$$
5	2 4	fmpti	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right):V⟶\mathrm{ran}\surd \cup \left\{\varnothing \right\}$$
6	1	fvexi	$$⊢V\in \mathrm{V}$$
7		cnex	$$⊢ℂ\in \mathrm{V}$$
8		sqrtf	$$⊢\surd :ℂ⟶ℂ$$
9		frn	$$⊢\surd :ℂ⟶ℂ\to \mathrm{ran}\surd \subseteq ℂ$$
10	8 9	ax-mp	$$⊢\mathrm{ran}\surd \subseteq ℂ$$
11	7 10	ssexi	$$⊢\mathrm{ran}\surd \in \mathrm{V}$$
12		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
13	11 12	unex	$$⊢\mathrm{ran}\surd \cup \left\{\varnothing \right\}\in \mathrm{V}$$
14		fex2	$$⊢\left(\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right):V⟶\mathrm{ran}\surd \cup \left\{\varnothing \right\}\wedge V\in \mathrm{V}\wedge \mathrm{ran}\surd \cup \left\{\varnothing \right\}\in \mathrm{V}\right)\to \left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\in \mathrm{V}$$
15	5 6 13 14	mp3an	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\in \mathrm{V}$$