ustuqtop2

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

Proof

Step	Hyp	Ref	Expression
1		utopustuq.1	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
2		simp-6l	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to (U \in UnifOn (X) \land p \in X)$
3		simp-7l	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to U \in UnifOn (X)$
4		simp-4r	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to w \in U$
5		simplr	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to u \in U$
6		ustincl	$⊢ (U \in UnifOn (X) \land w \in U \land u \in U) \to w \cap u \in U$
7	3 4 5 6	syl3anc	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to w \cap u \in U$
8		ineq12	$⊢ (a = w [\{p\}] \land b = u [\{p\}]) \to a \cap b = w [\{p\}] \cap u [\{p\}]$
9		inimasn	$⊢ p \in V \to (w \cap u) [\{p\}] = w [\{p\}] \cap u [\{p\}]$
10	9	elv	$⊢ (w \cap u) [\{p\}] = w [\{p\}] \cap u [\{p\}]$
11	8 10	eqtr4di	$⊢ (a = w [\{p\}] \land b = u [\{p\}]) \to a \cap b = (w \cap u) [\{p\}]$
12	11	ad4ant24	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to a \cap b = (w \cap u) [\{p\}]$
13		imaeq1	$⊢ x = w \cap u \to x [\{p\}] = (w \cap u) [\{p\}]$
14	13	rspceeqv	$⊢ (w \cap u \in U \land a \cap b = (w \cap u) [\{p\}]) \to \exists x \in U a \cap b = x [\{p\}]$
15	7 12 14	syl2anc	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to \exists x \in U a \cap b = x [\{p\}]$
16		vex	$⊢ a \in V$
17	16	inex1	$⊢ a \cap b \in V$
18	1	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \cap b \in V) \to (a \cap b \in N (p) \leftrightarrow \exists x \in U a \cap b = x [\{p\}])$
19	17 18	mpan2	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \cap b \in N (p) \leftrightarrow \exists x \in U a \cap b = x [\{p\}])$
20	19	biimpar	$⊢ ((U \in UnifOn (X) \land p \in X) \land \exists x \in U a \cap b = x [\{p\}]) \to a \cap b \in N (p)$
21	2 15 20	syl2anc	$⊢ (((((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \land u \in U) \land b = u [\{p\}]) \to a \cap b \in N (p)$
22	1	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land p \in X) \land b \in V) \to (b \in N (p) \leftrightarrow \exists u \in U b = u [\{p\}])$
23	22	elvd	$⊢ (U \in UnifOn (X) \land p \in X) \to (b \in N (p) \leftrightarrow \exists u \in U b = u [\{p\}])$
24	23	biimpa	$⊢ ((U \in UnifOn (X) \land p \in X) \land b \in N (p)) \to \exists u \in U b = u [\{p\}]$
25	24	ad5ant13	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \exists u \in U b = u [\{p\}]$
26	21 25	r19.29a	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \land w \in U) \land a = w [\{p\}]) \to a \cap b \in N (p)$
27	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\}])$
28	27	elvd	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \in N (p) \leftrightarrow \exists w \in U a = w [\{p\}])$
29	28	biimpa	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \exists w \in U a = w [\{p\}]$
30	29	adantr	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \to \exists w \in U a = w [\{p\}]$
31	26 30	r19.29a	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land b \in N (p)) \to a \cap b \in N (p)$
32	31	ralrimiva	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \forall b \in N (p) a \cap b \in N (p)$
33	32	ralrimiva	$⊢ (U \in UnifOn (X) \land p \in X) \to \forall a \in N (p) \forall b \in N (p) a \cap b \in N (p)$
34		fvex	$⊢ N (p) \in V$
35		inficl	$⊢ N (p) \in V \to (\forall a \in N (p) \forall b \in N (p) a \cap b \in N (p) \leftrightarrow fi (N (p)) = N (p))$
36	34 35	ax-mp	$⊢ \forall a \in N (p) \forall b \in N (p) a \cap b \in N (p) \leftrightarrow fi (N (p)) = N (p)$
37	33 36	sylib	$⊢ (U \in UnifOn (X) \land p \in X) \to fi (N (p)) = N (p)$
38		eqimss	$⊢ fi (N (p)) = N (p) \to fi (N (p)) \subseteq N (p)$
39	37 38	syl	$⊢ (U \in UnifOn (X) \land p \in X) \to fi (N (p)) \subseteq N (p)$

Metamath Proof Explorer

Theorem ustuqtop2

Proof