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