This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )