Theorem ustuqtop2

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

	Ref	Expression
Hypothesis	utopustuq.1	⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
Assertion	ustuqtop2	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )

Proof

Step	Hyp	Ref	Expression
1		utopustuq.1	⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2		simp-6l	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) )
3		simp-7l	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
4		simp-4r	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → 𝑤 ∈ 𝑈 )
5		simplr	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → 𝑢 ∈ 𝑈 )
6		ustincl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑤 ∩ 𝑢 ) ∈ 𝑈 )
7	3 4 5 6	syl3anc	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑤 ∩ 𝑢 ) ∈ 𝑈 )
8		ineq12	⊢ ( ( 𝑎 = ( 𝑤 “ { 𝑝 } ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 “ { 𝑝 } ) ∩ ( 𝑢 “ { 𝑝 } ) ) )
9		inimasn	⊢ ( 𝑝 ∈ V → ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) = ( ( 𝑤 “ { 𝑝 } ) ∩ ( 𝑢 “ { 𝑝 } ) ) )
10	9	elv	⊢ ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) = ( ( 𝑤 “ { 𝑝 } ) ∩ ( 𝑢 “ { 𝑝 } ) )
11	8 10	eqtr4di	⊢ ( ( 𝑎 = ( 𝑤 “ { 𝑝 } ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) )
12	11	ad4ant24	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) )
13		imaeq1	⊢ ( 𝑥 = ( 𝑤 ∩ 𝑢 ) → ( 𝑥 “ { 𝑝 } ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) )
14	13	rspceeqv	⊢ ( ( ( 𝑤 ∩ 𝑢 ) ∈ 𝑈 ∧ ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) ) → ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) )
15	7 12 14	syl2anc	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) )
16		vex	⊢ 𝑎 ∈ V
17	16	inex1	⊢ ( 𝑎 ∩ 𝑏 ) ∈ V
18	1	ustuqtoplem	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑎 ∩ 𝑏 ) ∈ V ) → ( ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) )
19	17 18	mpan2	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) )
20	19	biimpar	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) )
21	2 15 20	syl2anc	⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) )
22	1	ustuqtoplem	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑏 ∈ V ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) )
23	22	elvd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) )
24	23	biimpa	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) )
25	24	ad5ant13	⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) )
26	21 25	r19.29a	⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) )
27	1	ustuqtoplem	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ V ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
28	27	elvd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
29	28	biimpa	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) )
30	29	adantr	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) )
31	26 30	r19.29a	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) )
32	31	ralrimiva	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) )
33	32	ralrimiva	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ∀ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) )
34		fvex	⊢ ( 𝑁 ‘ 𝑝 ) ∈ V
35		inficl	⊢ ( ( 𝑁 ‘ 𝑝 ) ∈ V → ( ∀ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) ) )
36	34 35	ax-mp	⊢ ( ∀ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) )
37	33 36	sylib	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) )
38		eqimss	⊢ ( ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
39	37 38	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )