ustuqtop3

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

Proof

Step	Hyp	Ref	Expression
1		utopustuq.1	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
2		fnresi	$⊢ ({I ↾}_{X}) Fn X$
3		fnsnfv	$⊢ (({I ↾}_{X}) Fn X \land p \in X) \to \{({I ↾}_{X}) (p)\} = ({I ↾}_{X}) [\{p\}]$
4	2 3	mpan	$⊢ p \in X \to \{({I ↾}_{X}) (p)\} = ({I ↾}_{X}) [\{p\}]$
5	4	ad4antlr	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \{({I ↾}_{X}) (p)\} = ({I ↾}_{X}) [\{p\}]$
6		ustdiag	$⊢ (U \in UnifOn (X) \land w \in U) \to {I ↾}_{X} \subseteq w$
7	6	ad5ant14	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to {I ↾}_{X} \subseteq w$
8		imass1	$⊢ {I ↾}_{X} \subseteq w \to ({I ↾}_{X}) [\{p\}] \subseteq w [\{p\}]$
9	7 8	syl	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to ({I ↾}_{X}) [\{p\}] \subseteq w [\{p\}]$
10	5 9	eqsstrd	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \{({I ↾}_{X}) (p)\} \subseteq w [\{p\}]$
11		fvex	$⊢ ({I ↾}_{X}) (p) \in V$
12	11	snss	$⊢ ({I ↾}_{X}) (p) \in w [\{p\}] \leftrightarrow \{({I ↾}_{X}) (p)\} \subseteq w [\{p\}]$
13	10 12	sylibr	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to ({I ↾}_{X}) (p) \in w [\{p\}]$
14		fvresi	$⊢ p \in X \to ({I ↾}_{X}) (p) = p$
15	14	eqcomd	$⊢ p \in X \to p = ({I ↾}_{X}) (p)$
16	15	ad4antlr	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to p = ({I ↾}_{X}) (p)$
17		simpr	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to a = w [\{p\}]$
18	13 16 17	3eltr4d	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to p \in a$
19	1	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in V) \to (a \in N (p) \leftrightarrow \exists w \in U a = w [\{p\}])$
20	19	elvd	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \in N (p) \leftrightarrow \exists w \in U a = w [\{p\}])$
21	20	biimpa	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \exists w \in U a = w [\{p\}]$
22	18 21	r19.29a	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to p \in a$

Metamath Proof Explorer

Theorem ustuqtop3

Proof