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 \in V ⟼ \sqrt{x \underset{˙}{,} x}) \in V$

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

Metamath Proof Explorer