Theorem ustuqtoplem

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

	Ref	Expression
Hypothesis	utopustuq.1	|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
Assertion	ustuqtoplem	|- ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ A e. V ) -> ( A e. ( N ` P ) <-> E. w e. U A = ( w " { P } ) ) )

Proof

Step	Hyp	Ref	Expression
1		utopustuq.1	|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2		simpl	|- ( ( p = q /\ v e. U ) -> p = q )
3	2	sneqd	|- ( ( p = q /\ v e. U ) -> { p } = { q } )
4	3	imaeq2d	|- ( ( p = q /\ v e. U ) -> ( v " { p } ) = ( v " { q } ) )
5	4	mpteq2dva	|- ( p = q -> ( v e. U |-> ( v " { p } ) ) = ( v e. U |-> ( v " { q } ) ) )
6	5	rneqd	|- ( p = q -> ran ( v e. U |-> ( v " { p } ) ) = ran ( v e. U |-> ( v " { q } ) ) )
7	6	cbvmptv	|- ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) ) = ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) )
8	1 7	eqtri	|- N = ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) )
9		simpr2	|- ( ( U e. ( UnifOn ` X ) /\ ( P e. X /\ q = P /\ v e. U ) ) -> q = P )
10	9	sneqd	|- ( ( U e. ( UnifOn ` X ) /\ ( P e. X /\ q = P /\ v e. U ) ) -> { q } = { P } )
11	10	imaeq2d	|- ( ( U e. ( UnifOn ` X ) /\ ( P e. X /\ q = P /\ v e. U ) ) -> ( v " { q } ) = ( v " { P } ) )
12	11	3anassrs	|- ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ q = P ) /\ v e. U ) -> ( v " { q } ) = ( v " { P } ) )
13	12	mpteq2dva	|- ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ q = P ) -> ( v e. U |-> ( v " { q } ) ) = ( v e. U |-> ( v " { P } ) ) )
14	13	rneqd	|- ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ q = P ) -> ran ( v e. U |-> ( v " { q } ) ) = ran ( v e. U |-> ( v " { P } ) ) )
15		simpr	|- ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> P e. X )
16		mptexg	|- ( U e. ( UnifOn ` X ) -> ( v e. U |-> ( v " { P } ) ) e. _V )
17		rnexg	|- ( ( v e. U |-> ( v " { P } ) ) e. _V -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
18	16 17	syl	|- ( U e. ( UnifOn ` X ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
19	18	adantr	|- ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
20	8 14 15 19	fvmptd2	|- ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( N ` P ) = ran ( v e. U |-> ( v " { P } ) ) )
21	20	eleq2d	|- ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( A e. ( N ` P ) <-> A e. ran ( v e. U |-> ( v " { P } ) ) ) )
22		imaeq1	|- ( v = w -> ( v " { P } ) = ( w " { P } ) )
23	22	cbvmptv	|- ( v e. U |-> ( v " { P } ) ) = ( w e. U |-> ( w " { P } ) )
24	23	elrnmpt	|- ( A e. V -> ( A e. ran ( v e. U |-> ( v " { P } ) ) <-> E. w e. U A = ( w " { P } ) ) )
25	21 24	sylan9bb	|- ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ A e. V ) -> ( A e. ( N ` P ) <-> E. w e. U A = ( w " { P } ) ) )