Theorem ustuqtop4 19952

Description: Lemma for ustuqtop 19954 (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 757	. . . . . . . 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 754	. . . . . . . 8 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> u e. U )
3		eqid 2454	. . . . . . . . . . 11 |- ( u " { p } ) = ( u " { p } )
4		imaeq1 5273	. . . . . . . . . . . . 13 |- ( w = u -> ( w " { p } ) = ( u " { p } ) )
5	4	eqeq2d 2468	. . . . . . . . . . . 12 |- ( w = u -> ( ( u " { p } ) = ( w " { p } ) <-> ( u " { p } ) = ( u " { p } ) ) )
6	5	rspcev 3179	. . . . . . . . . . 11 |- ( ( u e. U /\ ( u " { p } ) = ( u " { p } ) ) -> E. w e. U ( u " { p } ) = ( w " { p } ) )
7	3, 6	mpan2 671	. . . . . . . . . 10 |- ( u e. U -> E. w e. U ( u " { p } ) = ( w " { p } ) )
8	7	adantl 466	. . . . . . . . 9 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> E. w e. U ( u " { p } ) = ( w " { p } ) )
9		imaexg 6626	. . . . . . . . . 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 19947	. . . . . . . . . 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 474	. . . . . . . . 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 232	. . . . . . . 8 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> ( u " { p } ) e. ( N ` p ) )
14	1, 2, 13	syl2anc 661	. . . . . . 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 767	. . . . . . . . . . . 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 459	. . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> p e. X )
18		ustimasn 19936	. . . . . . . . . . . . . 14 |- ( ( U e. (UnifOn ` X ) /\ u e. U /\ p e. X ) -> ( u " { p } ) C_ X )
19	16, 2, 17, 18	syl3anc 1219	. . . . . . . . . . . . 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 3465	. . . . . . . . . . . 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 532	. . . . . . . . . . 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 754	. . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . . . . . . 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 19919	. . . . . . . . . . . . . . . . . . 19 |- ( ( U e. (UnifOn ` X ) /\ u e. U ) -> Rel u )
26	23, 24, 25	syl2anc 661	. . . . . . . . . . . . . . . . . 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 5302	. . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . 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 5302	. . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . 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 3081	. . . . . . . . . . . . . . . . . . 19 |- p e. _V
35		vex 3081	. . . . . . . . . . . . . . . . . . 19 |- r e. _V
36	34, 35	brco 5119	. . . . . . . . . . . . . . . . . 18 |- ( p ( u o. u ) r <-> E. q ( p u q /\ q u r ) )
37	36	biimpri 206	. . . . . . . . . . . . . . . . 17 |- ( E. q ( p u q /\ q u r ) -> p ( u o. u ) r )
38	37	19.23bi 1810	. . . . . . . . . . . . . . . 16 |- ( ( p u q /\ q u r ) -> p ( u o. u ) r )
39	29, 33, 38	syl2anc 661	. . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . . 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 4442	. . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . 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 19919	. . . . . . . . . . . . . . . 16 |- ( ( U e. (UnifOn ` X ) /\ w e. U ) -> Rel w )
45	23, 43, 44	syl2anc 661	. . . . . . . . . . . . . . 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 5302	. . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . 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 434	. . . . . . . . . . . 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 3471	. . . . . . . . . . 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 766	. . . . . . . . . . . 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 465	. . . . . . . . . . . 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 19936	. . . . . . . . . . . 12 |- ( ( U e. (UnifOn ` X ) /\ w e. U /\ p e. X ) -> ( w " { p } ) C_ X )
54	15, 51, 52, 53	syl3anc 1219	. . . . . . . . . . 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 1168	. . . . . . . . . 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 758	. . . . . . . . . . 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 2455	. . . . . . . . . . . . . 14 |- ( u e. U -> ( u " { q } ) = ( u " { q } ) )
58		imaeq1 5273	. . . . . . . . . . . . . . . 16 |- ( w = u -> ( w " { q } ) = ( u " { q } ) )
59	58	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( w = u -> ( ( u " { q } ) = ( w " { q } ) <-> ( u " { q } ) = ( u " { q } ) ) )
60	59	rspcev 3179	. . . . . . . . . . . . . 14 |- ( ( u e. U /\ ( u " { q } ) = ( u " { q } ) ) -> E. w e. U ( u " { q } ) = ( w " { q } ) )
61	57, 60	mpdan 668	. . . . . . . . . . . . 13 |- ( u e. U -> E. w e. U ( u " { q } ) = ( w " { q } ) )
62	61	adantl 466	. . . . . . . . . . . 12 |- ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> E. w e. U ( u " { q } ) = ( w " { q } ) )
63		imaexg 6626	. . . . . . . . . . . . 13 |- ( u e. U -> ( u " { q } ) e. _V )
64	10	ustuqtoplem 19947	. . . . . . . . . . . . 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 474	. . . . . . . . . . . 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 232	. . . . . . . . . . 11 |- ( ( ( U e. (UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> ( u " { q } ) e. ( N ` q ) )
67	15, 20, 56, 66	syl21anc 1218	. . . . . . . . . 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 532	. . . . . . . . 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 6626	. . . . . . . . . . 11 |- ( w e. U -> ( w " { p } ) e. _V )
70		sseq2 3487	. . . . . . . . . . . . . . . 16 |- ( b = ( w " { p } ) -> ( ( u " { q } ) C_ b <-> ( u " { q } ) C_ ( w " { p } ) ) )
71		sseq1 3486	. . . . . . . . . . . . . . . 16 |- ( b = ( w " { p } ) -> ( b C_ X <-> ( w " { p } ) C_ X ) )
72	70, 71	3anbi23d 1293	. . . . . . . . . . . . . . 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 704	. . . . . . . . . . . . . 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 704	. . . . . . . . . . . . 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 2526	. . . . . . . . . . . . 13 |- ( b = ( w " { p } ) -> ( b e. ( N ` q ) <-> ( w " { p } ) e. ( N ` q ) ) )
76	74, 75	imbi12d 320	. . . . . . . . . . . 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 3486	. . . . . . . . . . . . . . . . . 18 |- ( a = ( u " { q } ) -> ( a C_ b <-> ( u " { q } ) C_ b ) )
78	77	3anbi2d 1295	. . . . . . . . . . . . . . . . 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 2526	. . . . . . . . . . . . . . . . 17 |- ( a = ( u " { q } ) -> ( a e. ( N ` q ) <-> ( u " { q } ) e. ( N ` q ) ) )
80	78, 79	anbi12d 710	. . . . . . . . . . . . . . . 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 317	. . . . . . . . . . . . . . 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 2526	. . . . . . . . . . . . . . . . . . . 20 |- ( p = q -> ( p e. X <-> q e. X ) )
83	82	anbi2d 703	. . . . . . . . . . . . . . . . . . 19 |- ( p = q -> ( ( U e. (UnifOn ` X ) /\ p e. X ) <-> ( U e. (UnifOn ` X ) /\ q e. X ) ) )
84	83	3anbi1d 1294	. . . . . . . . . . . . . . . . . 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 5800	. . . . . . . . . . . . . . . . . . 19 |- ( p = q -> ( N ` p ) = ( N ` q ) )
86	85	eleq2d 2524	. . . . . . . . . . . . . . . . . 18 |- ( p = q -> ( a e. ( N ` p ) <-> a e. ( N ` q ) ) )
87	84, 86	anbi12d 710	. . . . . . . . . . . . . . . . 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 2524	. . . . . . . . . . . . . . . . 17 |- ( p = q -> ( b e. ( N ` p ) <-> b e. ( N ` q ) ) )
89	87, 88	imbi12d 320	. . . . . . . . . . . . . . . 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 19949	. . . . . . . . . . . . . . . 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 1970	. . . . . . . . . . . . . . 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 3136	. . . . . . . . . . . . . 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 430	. . . . . . . . . . . 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 3136	. . . . . . . . . . 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 430	. . . . . . . . 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 1218	. . . . . . . 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 2830	. . . . . . 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 3023	. . . . . . . 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 3179	. . . . . . 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 661	. . . . . 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 19918	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ w e. U ) -> E. u e. U ( u o. u ) C_ w )
104	103	adantlr 714	. . . . . 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 2968	. . . . 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 465	. . . 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 2526	. . . . . 6 |- ( a = ( w " { p } ) -> ( a e. ( N ` q ) <-> ( w " { p } ) e. ( N ` q ) ) )
108	107	rexralbidv 2881	. . . . 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 466	. . . 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 232	. . 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 718	. 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 3081	. . . 4 |- a e. _V
113	10	ustuqtoplem 19947	. . . 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 671	. . 3 |- ( ( U e. (UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
115	114	biimpa 484	. 2 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
116	111, 115	r19.29a 2968	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 184   /\ wa 369   /\ w3a 965   = wceq 1370   E.wex 1587   e. wcel 1758   A.wral 2799   E.wrex 2800   _Vcvv 3078   C_ wss 3437   {csn 3986   class class class wbr 4401   |-> cmpt 4459   ran crn 4950   "cima 4952   o. ccom 4953   Rel wrel 4954   ` cfv 5527  UnifOncust 19907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4512  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-ust 19908

This theorem is referenced by:  ustuqtop  19954  utopsnneiplem  19955