Metamath Proof Explorer

Theorem ustuqtop1

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

Ref Expression
Hypothesis utopustuq.1 ⊢ N = p ∈ X ⟼ ran ⁡ v ∈ U ⟼ v p
Assertion ustuqtop1 ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X ∧ a ⊆ b ∧ b ⊆ X ∧ a ∈ N ⁡ p → b ∈ N ⁡ p

Proof

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