Theorem ustuqtop4 18227

Description: Lemma for ustuqtop 18229 (Contributed by Thierry Arnoux, 11-Jan-2018.)

Hypothesis

Ref	Expression
utopustuq.1	|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )

Assertion

Ref	Expression
ustuqtop4	|- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )

Distinct variable groups:   v, q, p, U   X, p, q, v   a, b, p, q, N   v, a, U, b   X, a, b

Allowed substitution hint:   N( v)

Proof of Theorem ustuqtop4

Dummy variables w r u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplll 735	. . . . . . . 8 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> ( U e. (UnifOn ` X ) /\ p e. X ) )
2		simplr 732	. . . . . . . 8 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> u e. U )
3		eqid 2404	. . . . . . . . . . 11 |- ( u " { p } ) = ( u " { p } )
4		imaeq1 5157	. . . . . . . . . . . . 13 |- ( w = u -> ( w " { p } ) = ( u " { p } ) )
5	4	eqeq2d 2415	. . . . . . . . . . . 12 |- ( w = u -> ( ( u " { p } ) = ( w " { p } ) <-> ( u " { p } ) = ( u " { p } ) ) )
6	5	rspcev 3012	. . . . . . . . . . 11 |- ( ( u e. U /\ ( u " { p } ) = ( u " { p } ) ) -> E. w e. U ( u " { p } ) = ( w " { p } ) )
7	3, 6	mpan2 653	. . . . . . . . . 10 |- ( u e. U -> E. w e. U ( u " { p } ) = ( w " { p } ) )
8	7	adantl 453	. . . . . . . . 9 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> E. w e. U ( u " { p } ) = ( w " { p } ) )
9		imaexg 5176	. . . . . . . . . 10 |- ( u e. U -> ( u " { p } ) e. _V )
10		utopustuq.1	. . . . . . . . . . 11 |- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
11	10	ustuqtoplem 18222	. . . . . . . . . 10 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ ( u " { p } ) e. _V ) -> ( ( u " { p } ) e. ( N ` p ) <-> E. w e. U ( u " { p } ) = ( w " { p } ) ) )
12	9, 11	sylan2 461	. . . . . . . . 9 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> ( ( u " { p } ) e. ( N ` p ) <-> E. w e. U ( u " { p } ) = ( w " { p } ) ) )
13	8, 12	mpbird 224	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> ( u " { p } ) e. ( N ` p ) )
14	1, 2, 13	syl2anc 643	. . . . . . 7 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> ( u " { p } ) e. ( N ` p ) )
15		simp-5l 745	. . . . . . . . . . . 12 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> U e. (UnifOn ` X ) )
16	1	simpld 446	. . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> U e. (UnifOn ` X ) )
17		simp-4r 744	. . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> p e. X )
18		ustimasn 18211	. . . . . . . . . . . . . 14 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ p e. X ) -> ( u " { p } ) C_ X )
19	16, 2, 17, 18	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> ( u " { p } ) C_ X )
20	19	sselda 3308	. . . . . . . . . . . 12 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> q e. X )
21	15, 20	jca 519	. . . . . . . . . . 11 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( U e. (UnifOn ` X ) /\ q e. X ) )
22		simplr 732	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> q e. ( u " { p } ) )
23		simp-6l 747	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> U e. (UnifOn ` X ) )
24		simp-4r 744	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> u e. U )
25		ustrel 18194	. . . . . . . . . . . . . . . . . . 19 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> Rel u )
26	23, 24, 25	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> Rel u )
27		elrelimasn 5187	. . . . . . . . . . . . . . . . . 18 |- ( Rel u -> ( q e. ( u " { p } ) <-> p u q ) )
28	26, 27	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( q e. ( u " { p } ) <-> p u q ) )
29	22, 28	mpbid 202	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> p u q )
30		simpr 448	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> r e. ( u " { q } ) )
31		elrelimasn 5187	. . . . . . . . . . . . . . . . . 18 |- ( Rel u -> ( r e. ( u " { q } ) <-> q u r ) )
32	26, 31	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( r e. ( u " { q } ) <-> q u r ) )
33	30, 32	mpbid 202	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> q u r )
34		vex 2919	. . . . . . . . . . . . . . . . . . 19 |- p e. _V
35		vex 2919	. . . . . . . . . . . . . . . . . . 19 |- r e. _V
36	34, 35	brco 5002	. . . . . . . . . . . . . . . . . 18 |- ( p ( u o. u ) r <-> E. q ( p u q /\ q u r ) )
37	36	biimpri 198	. . . . . . . . . . . . . . . . 17 |- ( E. q ( p u q /\ q u r ) -> p ( u o. u ) r )
38	37	19.23bi 1771	. . . . . . . . . . . . . . . 16 |- ( ( p u q /\ q u r ) -> p ( u o. u ) r )
39	29, 33, 38	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> p ( u o. u ) r )
40		simpllr 736	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( u o. u ) C_ w )
41	40	ssbrd 4213	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( p ( u o. u ) r -> p w r ) )
42	39, 41	mpd 15	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> p w r )
43		simp-5r 746	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> w e. U )
44		ustrel 18194	. . . . . . . . . . . . . . . 16 |- ( ( U e. (UnifOn ` X ) /\ w e. U ) -> Rel w )
45	23, 43, 44	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> Rel w )
46		elrelimasn 5187	. . . . . . . . . . . . . . 15 |- ( Rel w -> ( r e. ( w " { p } ) <-> p w r ) )
47	45, 46	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( r e. ( w " { p } ) <-> p w r ) )
48	42, 47	mpbird 224	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> r e. ( w " { p } ) )
49	48	ex 424	. . . . . . . . . . . 12 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( r e. ( u " { q } ) -> r e. ( w " { p } ) ) )
50	49	ssrdv 3314	. . . . . . . . . . 11 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( u " { q } ) C_ ( w " { p } ) )
51		simp-4r 744	. . . . . . . . . . . 12 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> w e. U )
52	17	adantr 452	. . . . . . . . . . . 12 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> p e. X )
53		ustimasn 18211	. . . . . . . . . . . 12 |- ( ( U e. (UnifOn ` X ) /\ w e. U /\ p e. X ) -> ( w " { p } ) C_ X )
54	15, 51, 52, 53	syl3anc 1184	. . . . . . . . . . 11 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( w " { p } ) C_ X )
55	21, 50, 54	3jca 1134	. . . . . . . . . 10 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) )
56		simpllr 736	. . . . . . . . . . 11 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> u e. U )
57		eqidd 2405	. . . . . . . . . . . . . 14 |- ( u e. U -> ( u " { q } ) = ( u " { q } ) )
58		imaeq1 5157	. . . . . . . . . . . . . . . 16 |- ( w = u -> ( w " { q } ) = ( u " { q } ) )
59	58	eqeq2d 2415	. . . . . . . . . . . . . . 15 |- ( w = u -> ( ( u " { q } ) = ( w " { q } ) <-> ( u " { q } ) = ( u " { q } ) ) )
60	59	rspcev 3012	. . . . . . . . . . . . . 14 |- ( ( u e. U /\ ( u " { q } ) = ( u " { q } ) ) -> E. w e. U ( u " { q } ) = ( w " { q } ) )
61	57, 60	mpdan 650	. . . . . . . . . . . . 13 |- ( u e. U -> E. w e. U ( u " { q } ) = ( w " { q } ) )
62	61	adantl 453	. . . . . . . . . . . 12 |- ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> E. w e. U ( u " { q } ) = ( w " { q } ) )
63		imaexg 5176	. . . . . . . . . . . . 13 |- ( u e. U -> ( u " { q } ) e. _V )
64	10	ustuqtoplem 18222	. . . . . . . . . . . . 13 |- ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) e. _V ) -> ( ( u " { q } ) e. ( N ` q ) <-> E. w e. U ( u " { q } ) = ( w " { q } ) ) )
65	63, 64	sylan2 461	. . . . . . . . . . . 12 |- ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> ( ( u " { q } ) e. ( N ` q ) <-> E. w e. U ( u " { q } ) = ( w " { q } ) ) )
66	62, 65	mpbird 224	. . . . . . . . . . 11 |- ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> ( u " { q } ) e. ( N ` q ) )
67	15, 20, 56, 66	syl21anc 1183	. . . . . . . . . 10 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( u " { q } ) e. ( N ` q ) )
68	55, 67	jca 519	. . . . . . . . 9 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) )
69		imaexg 5176	. . . . . . . . . . 11 |- ( w e. U -> ( w " { p } ) e. _V )
70		sseq2 3330	. . . . . . . . . . . . . . . 16 |- ( b = ( w " { p } ) -> ( ( u " { q } ) C_ b <-> ( u " { q } ) C_ ( w " { p } ) ) )
71		sseq1 3329	. . . . . . . . . . . . . . . 16 |- ( b = ( w " { p } ) -> ( b C_ X <-> ( w " { p } ) C_ X ) )
72	70, 71	3anbi23d 1257	. . . . . . . . . . . . . . 15 |- ( b = ( w " { p } ) -> ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) <-> ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) ) )
73	72	anbi1d 686	. . . . . . . . . . . . . 14 |- ( b = ( w " { p } ) -> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) <-> ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) ) )
74	73	anbi1d 686	. . . . . . . . . . . . 13 |- ( b = ( w " { p } ) -> ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) <-> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) ) )
75		eleq1 2464	. . . . . . . . . . . . 13 |- ( b = ( w " { p } ) -> ( b e. ( N ` q ) <-> ( w " { p } ) e. ( N ` q ) ) )
76	74, 75	imbi12d 312	. . . . . . . . . . . 12 |- ( b = ( w " { p } ) -> ( ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> b e. ( N ` q ) ) <-> ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> ( w " { p } ) e. ( N ` q ) ) ) )
77		sseq1 3329	. . . . . . . . . . . . . . . . . 18 |- ( a = ( u " { q } ) -> ( a C_ b <-> ( u " { q } ) C_ b ) )
78	77	3anbi2d 1259	. . . . . . . . . . . . . . . . 17 |- ( a = ( u " { q } ) -> ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) ) )
79		eleq1 2464	. . . . . . . . . . . . . . . . 17 |- ( a = ( u " { q } ) -> ( a e. ( N ` q ) <-> ( u " { q } ) e. ( N ` q ) ) )
80	78, 79	anbi12d 692	. . . . . . . . . . . . . . . 16 |- ( a = ( u " { q } ) -> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) <-> ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) ) )
81	80	imbi1d 309	. . . . . . . . . . . . . . 15 |- ( a = ( u " { q } ) -> ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) -> b e. ( N ` q ) ) <-> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) -> b e. ( N ` q ) ) ) )
82		eleq1 2464	. . . . . . . . . . . . . . . . . . . 20 |- ( p = q -> ( p e. X <-> q e. X ) )
83	82	anbi2d 685	. . . . . . . . . . . . . . . . . . 19 |- ( p = q -> ( ( U e. (UnifOn ` X ) /\ p e. X ) <-> ( U e. (UnifOn ` X ) /\ q e. X ) ) )
84	83	3anbi1d 1258	. . . . . . . . . . . . . . . . . 18 |- ( p = q -> ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) ) )
85		fveq2 5687	. . . . . . . . . . . . . . . . . . 19 |- ( p = q -> ( N ` p ) = ( N ` q ) )
86	85	eleq2d 2471	. . . . . . . . . . . . . . . . . 18 |- ( p = q -> ( a e. ( N ` p ) <-> a e. ( N ` q ) ) )
87	84, 86	anbi12d 692	. . . . . . . . . . . . . . . . 17 |- ( p = q -> ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) ) )
88	85	eleq2d 2471	. . . . . . . . . . . . . . . . 17 |- ( p = q -> ( b e. ( N ` p ) <-> b e. ( N ` q ) ) )
89	87, 88	imbi12d 312	. . . . . . . . . . . . . . . 16 |- ( p = q -> ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) ) <-> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) -> b e. ( N ` q ) ) ) )
90	10	ustuqtop1 18224	. . . . . . . . . . . . . . . 16 |- ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
91	89, 90	chvarv 2063	. . . . . . . . . . . . . . 15 |- ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) -> b e. ( N ` q ) )
92	81, 91	vtoclg 2971	. . . . . . . . . . . . . 14 |- ( ( u " { q } ) e. _V -> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) -> b e. ( N ` q ) ) )
93	63, 92	syl 16	. . . . . . . . . . . . 13 |- ( u e. U -> ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) -> b e. ( N ` q ) ) )
94	93	impcom 420	. . . . . . . . . . . 12 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> b e. ( N ` q ) )
95	76, 94	vtoclg 2971	. . . . . . . . . . 11 |- ( ( w " { p } ) e. _V -> ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> ( w " { p } ) e. ( N ` q ) ) )
96	69, 95	syl 16	. . . . . . . . . 10 |- ( w e. U -> ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> ( w " { p } ) e. ( N ` q ) ) )
97	96	impcom 420	. . . . . . . . 9 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) /\ w e. U ) -> ( w " { p } ) e. ( N ` q ) )
98	68, 56, 51, 97	syl21anc 1183	. . . . . . . 8 |- ( ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( w " { p } ) e. ( N ` q ) )
99	98	ralrimiva 2749	. . . . . . 7 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> A. q e. ( u " { p } ) ( w " { p } ) e. ( N ` q ) )
100		raleq 2864	. . . . . . . 8 |- ( b = ( u " { p } ) -> ( A. q e. b ( w " { p } ) e. ( N ` q ) <-> A. q e. ( u " { p } ) ( w " { p } ) e. ( N ` q ) ) )
101	100	rspcev 3012	. . . . . . 7 |- ( ( ( u " { p } ) e. ( N ` p ) /\ A. q e. ( u " { p } ) ( w " { p } ) e. ( N ` q ) ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
102	14, 99, 101	syl2anc 643	. . . . . 6 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
103		ustexhalf 18193	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ w e. U ) -> E. u e. U ( u o. u ) C_ w )
104	103	adantlr 696	. . . . . 6 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> E. u e. U ( u o. u ) C_ w )
105	102, 104	r19.29a 2810	. . . . 5 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
106	105	adantr 452	. . . 4 |- ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
107		eleq1 2464	. . . . . 6 |- ( a = ( w " { p } ) -> ( a e. ( N ` q ) <-> ( w " { p } ) e. ( N ` q ) ) )
108	107	rexralbidv 2710	. . . . 5 |- ( a = ( w " { p } ) -> ( E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) <-> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) ) )
109	108	adantl 453	. . . 4 |- ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) <-> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) ) )
110	106, 109	mpbird 224	. . 3 |- ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
111	110	adantllr 700	. 2 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
112		vex 2919	. . . 4 |- a e. _V
113	10	ustuqtoplem 18222	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
114	112, 113	mpan2 653	. . 3 |- ( ( U e. (UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
115	114	biimpa 471	. 2 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
116	111, 115	r19.29a 2810	1 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   _Vcvv 2916   C_ wss 3280   {csn 3774   class class class wbr 4172   e. cmpt 4226   ran crn 4838   "cima 4840   o. ccom 4841   Rel wrel 4842   ` cfv 5413  UnifOncust 18182

This theorem is referenced by:  ustuqtop  18229  utopsnneiplem  18230

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ust 18183