![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ustuqtop5 | Structured version Visualization version GIF version |
Description: Lemma for ustuqtop 22172. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
Ref | Expression |
---|---|
utopustuq.1 | ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
Ref | Expression |
---|---|
ustuqtop5 | ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ustbasel 22132 | . . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈) | |
2 | 1 | adantr 472 | . . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑋 × 𝑋) ∈ 𝑈) |
3 | snssi 4447 | . . . . . . . . 9 ⊢ (𝑝 ∈ 𝑋 → {𝑝} ⊆ 𝑋) | |
4 | dfss 3695 | . . . . . . . . 9 ⊢ ({𝑝} ⊆ 𝑋 ↔ {𝑝} = ({𝑝} ∩ 𝑋)) | |
5 | 3, 4 | sylib 208 | . . . . . . . 8 ⊢ (𝑝 ∈ 𝑋 → {𝑝} = ({𝑝} ∩ 𝑋)) |
6 | incom 3913 | . . . . . . . 8 ⊢ ({𝑝} ∩ 𝑋) = (𝑋 ∩ {𝑝}) | |
7 | 5, 6 | syl6req 2775 | . . . . . . 7 ⊢ (𝑝 ∈ 𝑋 → (𝑋 ∩ {𝑝}) = {𝑝}) |
8 | snnzg 4414 | . . . . . . 7 ⊢ (𝑝 ∈ 𝑋 → {𝑝} ≠ ∅) | |
9 | 7, 8 | eqnetrd 2963 | . . . . . 6 ⊢ (𝑝 ∈ 𝑋 → (𝑋 ∩ {𝑝}) ≠ ∅) |
10 | 9 | adantl 473 | . . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑋 ∩ {𝑝}) ≠ ∅) |
11 | xpima2 5688 | . . . . 5 ⊢ ((𝑋 ∩ {𝑝}) ≠ ∅ → ((𝑋 × 𝑋) “ {𝑝}) = 𝑋) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑋 × 𝑋) “ {𝑝}) = 𝑋) |
13 | 12 | eqcomd 2730 | . . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 = ((𝑋 × 𝑋) “ {𝑝})) |
14 | imaeq1 5571 | . . . . 5 ⊢ (𝑤 = (𝑋 × 𝑋) → (𝑤 “ {𝑝}) = ((𝑋 × 𝑋) “ {𝑝})) | |
15 | 14 | eqeq2d 2734 | . . . 4 ⊢ (𝑤 = (𝑋 × 𝑋) → (𝑋 = (𝑤 “ {𝑝}) ↔ 𝑋 = ((𝑋 × 𝑋) “ {𝑝}))) |
16 | 15 | rspcev 3413 | . . 3 ⊢ (((𝑋 × 𝑋) ∈ 𝑈 ∧ 𝑋 = ((𝑋 × 𝑋) “ {𝑝})) → ∃𝑤 ∈ 𝑈 𝑋 = (𝑤 “ {𝑝})) |
17 | 2, 13, 16 | syl2anc 696 | . 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ∃𝑤 ∈ 𝑈 𝑋 = (𝑤 “ {𝑝})) |
18 | elfvex 6334 | . . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V) | |
19 | utopustuq.1 | . . . 4 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) | |
20 | 19 | ustuqtoplem 22165 | . . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑋 ∈ V) → (𝑋 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑋 = (𝑤 “ {𝑝}))) |
21 | 18, 20 | mpidan 707 | . 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑋 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑋 = (𝑤 “ {𝑝}))) |
22 | 17, 21 | mpbird 247 | 1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1596 ∈ wcel 2103 ≠ wne 2896 ∃wrex 3015 Vcvv 3304 ∩ cin 3679 ⊆ wss 3680 ∅c0 4023 {csn 4285 ↦ cmpt 4837 × cxp 5216 ran crn 5219 “ cima 5221 ‘cfv 6001 UnifOncust 22125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-reu 3021 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-ust 22126 |
This theorem is referenced by: ustuqtop 22172 utopsnneiplem 22173 |
Copyright terms: Public domain | W3C validator |