Theorem ustuqtop3 21038

Description: Lemma for ustuqtop 21041, similar to elnei 19905 (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
ustuqtop3	|- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )

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

Allowed substitution hint:   N( v)

Proof of Theorem ustuqtop3

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnresi 5679	. . . . . . 7 |- ( _I |` X ) Fn X
2		fnsnfv 5909	. . . . . . 7 |- ( ( ( _I |` X ) Fn X /\ p e. X ) -> { ( ( _I |` X ) ` p ) } = ( ( _I |` X ) " { p } ) )
3	1, 2	mpan 668	. . . . . 6 |- ( p e. X -> { ( ( _I |` X ) ` p ) } = ( ( _I |` X ) " { p } ) )
4	3	ad4antlr 731	. . . . 5 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> { ( ( _I |` X ) ` p ) } = ( ( _I |` X ) " { p } ) )
5		simp-4l 768	. . . . . . 7 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> U e. (UnifOn ` X ) )
6		simplr 754	. . . . . . 7 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> w e. U )
7		ustdiag 21003	. . . . . . 7 |- ( ( U e. (UnifOn ` X ) /\ w e. U ) -> ( _I |` X ) C_ w )
8	5, 6, 7	syl2anc 659	. . . . . 6 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( _I |` X ) C_ w )
9		imass1 5191	. . . . . 6 |- ( ( _I |` X ) C_ w -> ( ( _I |` X ) " { p } ) C_ ( w " { p } ) )
10	8, 9	syl 17	. . . . 5 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( ( _I |` X ) " { p } ) C_ ( w " { p } ) )
11	4, 10	eqsstrd 3476	. . . 4 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> { ( ( _I |` X ) ` p ) } C_ ( w " { p } ) )
12		fvex 5859	. . . . 5 |- ( ( _I |` X ) ` p ) e. _V
13	12	snss 4096	. . . 4 |- ( ( ( _I |` X ) ` p ) e. ( w " { p } ) <-> { ( ( _I |` X ) ` p ) } C_ ( w " { p } ) )
14	11, 13	sylibr 212	. . 3 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( ( _I |` X ) ` p ) e. ( w " { p } ) )
15		fvresi 6077	. . . . 5 |- ( p e. X -> ( ( _I |` X ) ` p ) = p )
16	15	eqcomd 2410	. . . 4 |- ( p e. X -> p = ( ( _I |` X ) ` p ) )
17	16	ad4antlr 731	. . 3 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> p = ( ( _I |` X ) ` p ) )
18		simpr 459	. . 3 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> a = ( w " { p } ) )
19	14, 17, 18	3eltr4d 2505	. 2 |- ( ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> p e. a )
20		vex 3062	. . . 4 |- a e. _V
21		utopustuq.1	. . . . 5 |- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
22	21	ustuqtoplem 21034	. . . 4 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
23	20, 22	mpan2 669	. . 3 |- ( ( U e. (UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
24	23	biimpa 482	. 2 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
25	19, 24	r19.29a 2949	1 |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   E.wrex 2755   _Vcvv 3059   C_ wss 3414   {csn 3972   |-> cmpt 4453   _I cid 4733   ran crn 4824   |` cres 4825   "cima 4826   Fn wfn 5564   ` cfv 5569  UnifOncust 20994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ust 20995

This theorem is referenced by:  ustuqtop  21041  utopsnneiplem  21042