ustuqtop1

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

Proof

Step	Hyp	Ref	Expression
1		utopustuq.1	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
2		simpl1l	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land (a \in N (p) \land w \in U \land a = w [\{p\}])) \to U \in UnifOn (X)$
3	2	3anassrs	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to U \in UnifOn (X)$
4		simplr	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to w \in U$
5		ustssxp	$⊢ (U \in UnifOn (X) \land w \in U) \to w \subseteq X \times X$
6	3 4 5	syl2anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to w \subseteq X \times X$
7		simpl1r	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land (a \in N (p) \land w \in U \land a = w [\{p\}])) \to p \in X$
8	7	3anassrs	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to p \in X$
9	8	snssd	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \{p\} \subseteq X$
10		simpl3	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land (a \in N (p) \land w \in U \land a = w [\{p\}])) \to b \subseteq X$
11	10	3anassrs	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to b \subseteq X$
12		xpss12	$⊢ (\{p\} \subseteq X \land b \subseteq X) \to \{p\} \times b \subseteq X \times X$
13	9 11 12	syl2anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \{p\} \times b \subseteq X \times X$
14	6 13	unssd	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to w \cup (\{p\} \times b) \subseteq X \times X$
15		ssun1	$⊢ w \subseteq w \cup (\{p\} \times b)$
16	15	a1i	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to w \subseteq w \cup (\{p\} \times b)$
17		ustssel	$⊢ (U \in UnifOn (X) \land w \in U \land w \cup (\{p\} \times b) \subseteq X \times X) \to (w \subseteq w \cup (\{p\} \times b) \to w \cup (\{p\} \times b) \in U)$
18	17	imp	$⊢ ((U \in UnifOn (X) \land w \in U \land w \cup (\{p\} \times b) \subseteq X \times X) \land w \subseteq w \cup (\{p\} \times b)) \to w \cup (\{p\} \times b) \in U$
19	3 4 14 16 18	syl31anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to w \cup (\{p\} \times b) \in U$
20		simpl2	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land (a \in N (p) \land w \in U \land a = w [\{p\}])) \to a \subseteq b$
21	20	3anassrs	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to a \subseteq b$
22		ssequn1	$⊢ a \subseteq b \leftrightarrow a \cup b = b$
23	22	biimpi	$⊢ a \subseteq b \to a \cup b = b$
24		id	$⊢ a = w [\{p\}] \to a = w [\{p\}]$
25		inidm	$⊢ \{p\} \cap \{p\} = \{p\}$
26		vex	$⊢ p \in V$
27	26	snnz	$⊢ \{p\} \neq \emptyset$
28	25 27	eqnetri	$⊢ \{p\} \cap \{p\} \neq \emptyset$
29		xpima2	$⊢ \{p\} \cap \{p\} \neq \emptyset \to (\{p\} \times b) [\{p\}] = b$
30	28 29	mp1i	$⊢ a = w [\{p\}] \to (\{p\} \times b) [\{p\}] = b$
31	30	eqcomd	$⊢ a = w [\{p\}] \to b = (\{p\} \times b) [\{p\}]$
32	24 31	uneq12d	$⊢ a = w [\{p\}] \to a \cup b = w [\{p\}] \cup (\{p\} \times b) [\{p\}]$
33		imaundir	$⊢ (w \cup (\{p\} \times b)) [\{p\}] = w [\{p\}] \cup (\{p\} \times b) [\{p\}]$
34	32 33	eqtr4di	$⊢ a = w [\{p\}] \to a \cup b = (w \cup (\{p\} \times b)) [\{p\}]$
35	23 34	sylan9req	$⊢ (a \subseteq b \land a = w [\{p\}]) \to b = (w \cup (\{p\} \times b)) [\{p\}]$
36	21 35	sylancom	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to b = (w \cup (\{p\} \times b)) [\{p\}]$
37		imaeq1	$⊢ u = w \cup (\{p\} \times b) \to u [\{p\}] = (w \cup (\{p\} \times b)) [\{p\}]$
38	37	rspceeqv	$⊢ (w \cup (\{p\} \times b) \in U \land b = (w \cup (\{p\} \times b)) [\{p\}]) \to \exists u \in U b = u [\{p\}]$
39	19 36 38	syl2anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \exists u \in U b = u [\{p\}]$
40	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\}])$
41	40	elvd	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \in N (p) \leftrightarrow \exists w \in U a = w [\{p\}])$
42	41	biimpa	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \exists w \in U a = w [\{p\}]$
43	42	3ad2antl1	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to \exists w \in U a = w [\{p\}]$
44	39 43	r19.29a	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to \exists u \in U b = u [\{p\}]$
45	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\}])$
46	45	elvd	$⊢ (U \in UnifOn (X) \land p \in X) \to (b \in N (p) \leftrightarrow \exists u \in U b = u [\{p\}])$
47	46	3ad2ant1	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \to (b \in N (p) \leftrightarrow \exists u \in U b = u [\{p\}])$
48	47	adantr	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to (b \in N (p) \leftrightarrow \exists u \in U b = u [\{p\}])$
49	44 48	mpbird	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)$

Metamath Proof Explorer

Theorem ustuqtop1

Proof