Metamath Proof Explorer

Theorem ustuqtop1

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

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

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 simpl1l ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑤 ∈ 𝑈 ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
3 2 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
4 simplr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑤 ∈ 𝑈 )
5 ustssxp ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
6 3 4 5 syl2anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
7 simpl1r ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑤 ∈ 𝑈 ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ) → 𝑝 ∈ 𝑋 )
8 7 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑝 ∈ 𝑋 )
9 8 snssd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → { 𝑝 } ⊆ 𝑋 )
10 simpl3 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑤 ∈ 𝑈 ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ) → 𝑏 ⊆ 𝑋 )
11 10 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑏 ⊆ 𝑋 )
12 xpss12 ⊢ ( ( { 𝑝 } ⊆ 𝑋 ∧ 𝑏 ⊆ 𝑋 ) → ( { 𝑝 } × 𝑏 ) ⊆ ( 𝑋 × 𝑋 ) )
13 9 11 12 syl2anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( { 𝑝 } × 𝑏 ) ⊆ ( 𝑋 × 𝑋 ) )
14 6 13 unssd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ⊆ ( 𝑋 × 𝑋 ) )
15 ssun1 ⊢ 𝑤 ⊆ ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) )
16 15 a1i ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑤 ⊆ ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) )
17 ustssel ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ∧ ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑤 ⊆ ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) → ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ∈ 𝑈 ) )
18 17 imp ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ∧ ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑤 ⊆ ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ) → ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ∈ 𝑈 )
19 3 4 14 16 18 syl31anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ∈ 𝑈 )
20 simpl2 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑤 ∈ 𝑈 ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ) → 𝑎 ⊆ 𝑏 )
21 20 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑎 ⊆ 𝑏 )
22 ssequn1 ⊢ ( 𝑎 ⊆ 𝑏 ↔ ( 𝑎 ∪ 𝑏 ) = 𝑏 )
23 22 biimpi ⊢ ( 𝑎 ⊆ 𝑏 → ( 𝑎 ∪ 𝑏 ) = 𝑏 )
24 id ⊢ ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → 𝑎 = ( 𝑤 “ { 𝑝 } ) )
25 inidm ⊢ ( { 𝑝 } ∩ { 𝑝 } ) = { 𝑝 }
26 vex ⊢ 𝑝 ∈ V
27 26 snnz ⊢ { 𝑝 } ≠ ∅
28 25 27 eqnetri ⊢ ( { 𝑝 } ∩ { 𝑝 } ) ≠ ∅
29 xpima2 ⊢ ( ( { 𝑝 } ∩ { 𝑝 } ) ≠ ∅ → ( ( { 𝑝 } × 𝑏 ) “ { 𝑝 } ) = 𝑏 )
30 28 29 mp1i ⊢ ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → ( ( { 𝑝 } × 𝑏 ) “ { 𝑝 } ) = 𝑏 )
31 30 eqcomd ⊢ ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → 𝑏 = ( ( { 𝑝 } × 𝑏 ) “ { 𝑝 } ) )
32 24 31 uneq12d ⊢ ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → ( 𝑎 ∪ 𝑏 ) = ( ( 𝑤 “ { 𝑝 } ) ∪ ( ( { 𝑝 } × 𝑏 ) “ { 𝑝 } ) ) )
33 imaundir ⊢ ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) “ { 𝑝 } ) = ( ( 𝑤 “ { 𝑝 } ) ∪ ( ( { 𝑝 } × 𝑏 ) “ { 𝑝 } ) )
34 32 33 eqtr4di ⊢ ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → ( 𝑎 ∪ 𝑏 ) = ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) “ { 𝑝 } ) )
35 23 34 sylan9req ⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑏 = ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) “ { 𝑝 } ) )
36 21 35 sylancom ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑏 = ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) “ { 𝑝 } ) )
37 imaeq1 ⊢ ( 𝑢 = ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) → ( 𝑢 “ { 𝑝 } ) = ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) “ { 𝑝 } ) )
38 37 rspceeqv ⊢ ( ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) ∈ 𝑈 ∧ 𝑏 = ( ( 𝑤 ∪ ( { 𝑝 } × 𝑏 ) ) “ { 𝑝 } ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) )
39 19 36 38 syl2anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) )
40 1 ustuqtoplem ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ V ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
41 40 elvd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
42 41 biimpa ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) )
43 42 3ad2antl1 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) )
44 39 43 r19.29a ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) )
45 1 ustuqtoplem ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑏 ∈ V ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) )
46 45 elvd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) )
47 46 3ad2ant1 ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) )
48 47 adantr ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) )
49 44 48 mpbird ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )