ustuqtop5

		Ref	Expression
	Hypothesis	utopustuq.1	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
	Assertion	ustuqtop5	$⊢ (U \in UnifOn (X) \land p \in X) \to X \in N (p)$

Step	Hyp	Ref	Expression
1		utopustuq.1	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
2		ustbasel	$⊢ U \in UnifOn (X) \to X \times X \in U$
3		snssi	$⊢ p \in X \to \{p\} \subseteq X$
4		dfss	$⊢ \{p\} \subseteq X \leftrightarrow \{p\} = \{p\} \cap X$
5	3 4	sylib	$⊢ p \in X \to \{p\} = \{p\} \cap X$
6		incom	$⊢ \{p\} \cap X = X \cap \{p\}$
7	5 6	eqtr2di	$⊢ p \in X \to X \cap \{p\} = \{p\}$
8		snnzg	$⊢ p \in X \to \{p\} \neq \emptyset$
9	7 8	eqnetrd	$⊢ p \in X \to X \cap \{p\} \neq \emptyset$
10	9	adantl	$⊢ (U \in UnifOn (X) \land p \in X) \to X \cap \{p\} \neq \emptyset$
11		xpima2	$⊢ X \cap \{p\} \neq \emptyset \to (X \times X) [\{p\}] = X$
12	10 11	syl	$⊢ (U \in UnifOn (X) \land p \in X) \to (X \times X) [\{p\}] = X$
13	12	eqcomd	$⊢ (U \in UnifOn (X) \land p \in X) \to X = (X \times X) [\{p\}]$
14		imaeq1	$⊢ w = X \times X \to w [\{p\}] = (X \times X) [\{p\}]$
15	14	rspceeqv	$⊢ (X \times X \in U \land X = (X \times X) [\{p\}]) \to \exists w \in U X = w [\{p\}]$
16	2 13 15	syl2an2r	$⊢ (U \in UnifOn (X) \land p \in X) \to \exists w \in U X = w [\{p\}]$
17		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
18	1	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land p \in X) \land X \in V) \to (X \in N (p) \leftrightarrow \exists w \in U X = w [\{p\}])$
19	17 18	mpidan	$⊢ (U \in UnifOn (X) \land p \in X) \to (X \in N (p) \leftrightarrow \exists w \in U X = w [\{p\}])$
20	16 19	mpbird	$⊢ (U \in UnifOn (X) \land p \in X) \to X \in N (p)$

Metamath Proof Explorer