ustuqtop4

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

Proof

Step	Hyp	Ref	Expression
1		utopustuq.1	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
2		simplll	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to (U \in UnifOn (X) \land p \in X)$
3		simplr	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to u \in U$
4		eqid	$⊢ u [\{p\}] = u [\{p\}]$
5		imaeq1	$⊢ w = u \to w [\{p\}] = u [\{p\}]$
6	5	rspceeqv	$⊢ (u \in U \land u [\{p\}] = u [\{p\}]) \to \exists w \in U u [\{p\}] = w [\{p\}]$
7	4 6	mpan2	$⊢ u \in U \to \exists w \in U u [\{p\}] = w [\{p\}]$
8	7	adantl	$⊢ ((U \in UnifOn (X) \land p \in X) \land u \in U) \to \exists w \in U u [\{p\}] = w [\{p\}]$
9		imaexg	$⊢ u \in U \to u [\{p\}] \in V$
10	1	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land p \in X) \land u [\{p\}] \in V) \to (u [\{p\}] \in N (p) \leftrightarrow \exists w \in U u [\{p\}] = w [\{p\}])$
11	9 10	sylan2	$⊢ ((U \in UnifOn (X) \land p \in X) \land u \in U) \to (u [\{p\}] \in N (p) \leftrightarrow \exists w \in U u [\{p\}] = w [\{p\}])$
12	8 11	mpbird	$⊢ ((U \in UnifOn (X) \land p \in X) \land u \in U) \to u [\{p\}] \in N (p)$
13	2 3 12	syl2anc	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to u [\{p\}] \in N (p)$
14		simp-5l	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to U \in UnifOn (X)$
15	2	simpld	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to U \in UnifOn (X)$
16		simp-4r	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to p \in X$
17		ustimasn	$⊢ (U \in UnifOn (X) \land u \in U \land p \in X) \to u [\{p\}] \subseteq X$
18	15 3 16 17	syl3anc	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to u [\{p\}] \subseteq X$
19	18	sselda	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to q \in X$
20	14 19	jca	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to (U \in UnifOn (X) \land q \in X)$
21		simplr	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to q \in u [\{p\}]$
22		simp-6l	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to U \in UnifOn (X)$
23		simp-4r	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to u \in U$
24		ustrel	$⊢ (U \in UnifOn (X) \land u \in U) \to Rel u$
25	22 23 24	syl2anc	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to Rel u$
26		elrelimasn	$⊢ Rel u \to (q \in u [\{p\}] \leftrightarrow p u q)$
27	25 26	syl	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to (q \in u [\{p\}] \leftrightarrow p u q)$
28	21 27	mpbid	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to p u q$
29		simpr	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to r \in u [\{q\}]$
30		elrelimasn	$⊢ Rel u \to (r \in u [\{q\}] \leftrightarrow q u r)$
31	25 30	syl	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to (r \in u [\{q\}] \leftrightarrow q u r)$
32	29 31	mpbid	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to q u r$
33		vex	$⊢ p \in V$
34		vex	$⊢ r \in V$
35	33 34	brco	$⊢ p (u \circ u) r \leftrightarrow \exists q (p u q \land q u r)$
36	35	biimpri	$⊢ \exists q (p u q \land q u r) \to p (u \circ u) r$
37	36	19.23bi	$⊢ (p u q \land q u r) \to p (u \circ u) r$
38	28 32 37	syl2anc	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to p (u \circ u) r$
39		simpllr	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to u \circ u \subseteq w$
40	39	ssbrd	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to (p (u \circ u) r \to p w r)$
41	38 40	mpd	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to p w r$
42		simp-5r	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to w \in U$
43		ustrel	$⊢ (U \in UnifOn (X) \land w \in U) \to Rel w$
44	22 42 43	syl2anc	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to Rel w$
45		elrelimasn	$⊢ Rel w \to (r \in w [\{p\}] \leftrightarrow p w r)$
46	44 45	syl	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to (r \in w [\{p\}] \leftrightarrow p w r)$
47	41 46	mpbird	$⊢ ((((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \land r \in u [\{q\}]) \to r \in w [\{p\}]$
48	47	ex	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to (r \in u [\{q\}] \to r \in w [\{p\}])$
49	48	ssrdv	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to u [\{q\}] \subseteq w [\{p\}]$
50		simp-4r	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to w \in U$
51	16	adantr	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to p \in X$
52		ustimasn	$⊢ (U \in UnifOn (X) \land w \in U \land p \in X) \to w [\{p\}] \subseteq X$
53	14 50 51 52	syl3anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to w [\{p\}] \subseteq X$
54	20 49 53	3jca	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to ((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X)$
55		simpllr	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to u \in U$
56		eqidd	$⊢ u \in U \to u [\{q\}] = u [\{q\}]$
57		imaeq1	$⊢ w = u \to w [\{q\}] = u [\{q\}]$
58	57	rspceeqv	$⊢ (u \in U \land u [\{q\}] = u [\{q\}]) \to \exists w \in U u [\{q\}] = w [\{q\}]$
59	56 58	mpdan	$⊢ u \in U \to \exists w \in U u [\{q\}] = w [\{q\}]$
60	59	adantl	$⊢ ((U \in UnifOn (X) \land q \in X) \land u \in U) \to \exists w \in U u [\{q\}] = w [\{q\}]$
61		imaexg	$⊢ u \in U \to u [\{q\}] \in V$
62	1	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \in V) \to (u [\{q\}] \in N (q) \leftrightarrow \exists w \in U u [\{q\}] = w [\{q\}])$
63	61 62	sylan2	$⊢ ((U \in UnifOn (X) \land q \in X) \land u \in U) \to (u [\{q\}] \in N (q) \leftrightarrow \exists w \in U u [\{q\}] = w [\{q\}])$
64	60 63	mpbird	$⊢ ((U \in UnifOn (X) \land q \in X) \land u \in U) \to u [\{q\}] \in N (q)$
65	14 19 55 64	syl21anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to u [\{q\}] \in N (q)$
66	54 65	jca	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to (((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q))$
67		imaexg	$⊢ w \in U \to w [\{p\}] \in V$
68		sseq2	$⊢ b = w [\{p\}] \to (u [\{q\}] \subseteq b \leftrightarrow u [\{q\}] \subseteq w [\{p\}])$
69		sseq1	$⊢ b = w [\{p\}] \to (b \subseteq X \leftrightarrow w [\{p\}] \subseteq X)$
70	68 69	3anbi23d	$⊢ b = w [\{p\}] \to (((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \leftrightarrow ((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X))$
71	70	anbi1d	$⊢ b = w [\{p\}] \to ((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \leftrightarrow (((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q)))$
72	71	anbi1d	$⊢ b = w [\{p\}] \to (((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \leftrightarrow ((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U))$
73		eleq1	$⊢ b = w [\{p\}] \to (b \in N (q) \leftrightarrow w [\{p\}] \in N (q))$
74	72 73	imbi12d	$⊢ b = w [\{p\}] \to ((((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \to b \in N (q)) \leftrightarrow (((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \to w [\{p\}] \in N (q)))$
75		sseq1	$⊢ a = u [\{q\}] \to (a \subseteq b \leftrightarrow u [\{q\}] \subseteq b)$
76	75	3anbi2d	$⊢ a = u [\{q\}] \to (((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X) \leftrightarrow ((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X))$
77		eleq1	$⊢ a = u [\{q\}] \to (a \in N (q) \leftrightarrow u [\{q\}] \in N (q))$
78	76 77	anbi12d	$⊢ a = u [\{q\}] \to ((((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (q)) \leftrightarrow (((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)))$
79	78	imbi1d	$⊢ a = u [\{q\}] \to (((((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (q)) \to b \in N (q)) \leftrightarrow ((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \to b \in N (q)))$
80		eleq1	$⊢ p = q \to (p \in X \leftrightarrow q \in X)$
81	80	anbi2d	$⊢ p = q \to ((U \in UnifOn (X) \land p \in X) \leftrightarrow (U \in UnifOn (X) \land q \in X))$
82	81	3anbi1d	$⊢ p = q \to (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \leftrightarrow ((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X))$
83		fveq2	$⊢ p = q \to N (p) = N (q)$
84	83	eleq2d	$⊢ p = q \to (a \in N (p) \leftrightarrow a \in N (q))$
85	82 84	anbi12d	$⊢ p = q \to ((((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \leftrightarrow (((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (q)))$
86	83	eleq2d	$⊢ p = q \to (b \in N (p) \leftrightarrow b \in N (q))$
87	85 86	imbi12d	$⊢ p = q \to (((((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 ((((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (q)) \to b \in N (q)))$
88	1	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)$
89	87 88	chvarvv	$⊢ (((U \in UnifOn (X) \land q \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (q)) \to b \in N (q)$
90	79 89	vtoclg	$⊢ u [\{q\}] \in V \to ((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \to b \in N (q))$
91	61 90	syl	$⊢ u \in U \to ((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \to b \in N (q))$
92	91	impcom	$⊢ ((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq b \land b \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \to b \in N (q)$
93	74 92	vtoclg	$⊢ w [\{p\}] \in V \to (((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \to w [\{p\}] \in N (q))$
94	67 93	syl	$⊢ w \in U \to (((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \to w [\{p\}] \in N (q))$
95	94	impcom	$⊢ (((((U \in UnifOn (X) \land q \in X) \land u [\{q\}] \subseteq w [\{p\}] \land w [\{p\}] \subseteq X) \land u [\{q\}] \in N (q)) \land u \in U) \land w \in U) \to w [\{p\}] \in N (q)$
96	66 55 50 95	syl21anc	$⊢ (((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \land q \in u [\{p\}]) \to w [\{p\}] \in N (q)$
97	96	ralrimiva	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to \forall q \in u [\{p\}] w [\{p\}] \in N (q)$
98		raleq	$⊢ b = u [\{p\}] \to (\forall q \in b w [\{p\}] \in N (q) \leftrightarrow \forall q \in u [\{p\}] w [\{p\}] \in N (q))$
99	98	rspcev	$⊢ (u [\{p\}] \in N (p) \land \forall q \in u [\{p\}] w [\{p\}] \in N (q)) \to \exists b \in N (p) \forall q \in b w [\{p\}] \in N (q)$
100	13 97 99	syl2anc	$⊢ ((((U \in UnifOn (X) \land p \in X) \land w \in U) \land u \in U) \land u \circ u \subseteq w) \to \exists b \in N (p) \forall q \in b w [\{p\}] \in N (q)$
101		ustexhalf	$⊢ (U \in UnifOn (X) \land w \in U) \to \exists u \in U u \circ u \subseteq w$
102	101	adantlr	$⊢ ((U \in UnifOn (X) \land p \in X) \land w \in U) \to \exists u \in U u \circ u \subseteq w$
103	100 102	r19.29a	$⊢ ((U \in UnifOn (X) \land p \in X) \land w \in U) \to \exists b \in N (p) \forall q \in b w [\{p\}] \in N (q)$
104	103	adantr	$⊢ (((U \in UnifOn (X) \land p \in X) \land w \in U) \land a = w [\{p\}]) \to \exists b \in N (p) \forall q \in b w [\{p\}] \in N (q)$
105		eleq1	$⊢ a = w [\{p\}] \to (a \in N (q) \leftrightarrow w [\{p\}] \in N (q))$
106	105	rexralbidv	$⊢ a = w [\{p\}] \to (\exists b \in N (p) \forall q \in b a \in N (q) \leftrightarrow \exists b \in N (p) \forall q \in b w [\{p\}] \in N (q))$
107	106	adantl	$⊢ (((U \in UnifOn (X) \land p \in X) \land w \in U) \land a = w [\{p\}]) \to (\exists b \in N (p) \forall q \in b a \in N (q) \leftrightarrow \exists b \in N (p) \forall q \in b w [\{p\}] \in N (q))$
108	104 107	mpbird	$⊢ (((U \in UnifOn (X) \land p \in X) \land w \in U) \land a = w [\{p\}]) \to \exists b \in N (p) \forall q \in b a \in N (q)$
109	108	adantllr	$⊢ ((((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \land w \in U) \land a = w [\{p\}]) \to \exists b \in N (p) \forall q \in b a \in N (q)$
110		vex	$⊢ a \in V$
111	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\}])$
112	110 111	mpan2	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \in N (p) \leftrightarrow \exists w \in U a = w [\{p\}])$
113	112	biimpa	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \exists w \in U a = w [\{p\}]$
114	109 113	r19.29a	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)$

Metamath Proof Explorer

Theorem ustuqtop4

Proof