Metamath Proof Explorer

Theorem dissneqlem

Description: This is the core of the proof of dissneq , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020)

Ref Expression
Hypothesis dissneq.c ⊢ C = u | ∃ x ∈ A u = x
Assertion dissneqlem ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → B = 𝒫 A

Proof

Step Hyp Ref Expression
1 dissneq.c ⊢ C = u | ∃ x ∈ A u = x
2 topgele ⊢ B ∈ TopOn ⁡ A → ∅ A ⊆ B ∧ B ⊆ 𝒫 A
3 2 adantl ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → ∅ A ⊆ B ∧ B ⊆ 𝒫 A
4 3 simprd ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → B ⊆ 𝒫 A
5 velpw ⊢ x ∈ 𝒫 A ↔ x ⊆ A
6 simp3 ⊢ C ⊆ B ∧ x ⊆ A ∧ B ∈ TopOn ⁡ A → B ∈ TopOn ⁡ A
7 df-ima ⊢ z ∈ A ⟼ z x = ran ⁡ z ∈ A ⟼ z ↾ x
8 resmpt ⊢ x ⊆ A → z ∈ A ⟼ z ↾ x = z ∈ x ⟼ z
9 8 rneqd ⊢ x ⊆ A → ran ⁡ z ∈ A ⟼ z ↾ x = ran ⁡ z ∈ x ⟼ z
10 7 9 syl5eq ⊢ x ⊆ A → z ∈ A ⟼ z x = ran ⁡ z ∈ x ⟼ z
11 rnmptsn ⊢ ran ⁡ z ∈ x ⟼ z = u | ∃ z ∈ x u = z
12 10 11 eqtrdi ⊢ x ⊆ A → z ∈ A ⟼ z x = u | ∃ z ∈ x u = z
13 imassrn ⊢ z ∈ A ⟼ z x ⊆ ran ⁡ z ∈ A ⟼ z
14 12 13 eqsstrrdi ⊢ x ⊆ A → u | ∃ z ∈ x u = z ⊆ ran ⁡ z ∈ A ⟼ z
15 rnmptsn ⊢ ran ⁡ z ∈ A ⟼ z = u | ∃ z ∈ A u = z
16 14 15 sseqtrdi ⊢ x ⊆ A → u | ∃ z ∈ x u = z ⊆ u | ∃ z ∈ A u = z
17 sneq ⊢ x = z → x = z
18 17 eqeq2d ⊢ x = z → u = x ↔ u = z
19 18 cbvrexvw ⊢ ∃ x ∈ A u = x ↔ ∃ z ∈ A u = z
20 19 abbii ⊢ u | ∃ x ∈ A u = x = u | ∃ z ∈ A u = z
21 1 20 eqtri ⊢ C = u | ∃ z ∈ A u = z
22 16 21 sseqtrrdi ⊢ x ⊆ A → u | ∃ z ∈ x u = z ⊆ C
23 22 adantl ⊢ C ⊆ B ∧ x ⊆ A → u | ∃ z ∈ x u = z ⊆ C
24 sstr ⊢ u | ∃ z ∈ x u = z ⊆ C ∧ C ⊆ B → u | ∃ z ∈ x u = z ⊆ B
25 24 expcom ⊢ C ⊆ B → u | ∃ z ∈ x u = z ⊆ C → u | ∃ z ∈ x u = z ⊆ B
26 25 adantr ⊢ C ⊆ B ∧ x ⊆ A → u | ∃ z ∈ x u = z ⊆ C → u | ∃ z ∈ x u = z ⊆ B
27 23 26 mpd ⊢ C ⊆ B ∧ x ⊆ A → u | ∃ z ∈ x u = z ⊆ B
28 27 3adant3 ⊢ C ⊆ B ∧ x ⊆ A ∧ B ∈ TopOn ⁡ A → u | ∃ z ∈ x u = z ⊆ B
29 6 28 ssexd ⊢ C ⊆ B ∧ x ⊆ A ∧ B ∈ TopOn ⁡ A → u | ∃ z ∈ x u = z ∈ V
30 isset ⊢ u | ∃ z ∈ x u = z ∈ V ↔ ∃ y y = u | ∃ z ∈ x u = z
31 29 30 sylib ⊢ C ⊆ B ∧ x ⊆ A ∧ B ∈ TopOn ⁡ A → ∃ y y = u | ∃ z ∈ x u = z
32 eqid ⊢ z ∈ A ⟼ z = z ∈ A ⟼ z
33 eqid ⊢ u | ∃ z ∈ A u = z = u | ∃ z ∈ A u = z
34 32 33 mptsnun ⊢ x ⊆ A → x = ⋃ z ∈ A ⟼ z x
35 12 unieqd ⊢ x ⊆ A → ⋃ z ∈ A ⟼ z x = ⋃ u | ∃ z ∈ x u = z
36 34 35 eqtrd ⊢ x ⊆ A → x = ⋃ u | ∃ z ∈ x u = z
37 36 adantl ⊢ C ⊆ B ∧ x ⊆ A → x = ⋃ u | ∃ z ∈ x u = z
38 27 37 jca ⊢ C ⊆ B ∧ x ⊆ A → u | ∃ z ∈ x u = z ⊆ B ∧ x = ⋃ u | ∃ z ∈ x u = z
39 sseq1 ⊢ y = u | ∃ z ∈ x u = z → y ⊆ B ↔ u | ∃ z ∈ x u = z ⊆ B
40 unieq ⊢ y = u | ∃ z ∈ x u = z → ⋃ y = ⋃ u | ∃ z ∈ x u = z
41 40 eqeq2d ⊢ y = u | ∃ z ∈ x u = z → x = ⋃ y ↔ x = ⋃ u | ∃ z ∈ x u = z
42 39 41 anbi12d ⊢ y = u | ∃ z ∈ x u = z → y ⊆ B ∧ x = ⋃ y ↔ u | ∃ z ∈ x u = z ⊆ B ∧ x = ⋃ u | ∃ z ∈ x u = z
43 38 42 syl5ibrcom ⊢ C ⊆ B ∧ x ⊆ A → y = u | ∃ z ∈ x u = z → y ⊆ B ∧ x = ⋃ y
44 43 eximdv ⊢ C ⊆ B ∧ x ⊆ A → ∃ y y = u | ∃ z ∈ x u = z → ∃ y y ⊆ B ∧ x = ⋃ y
45 44 3adant3 ⊢ C ⊆ B ∧ x ⊆ A ∧ B ∈ TopOn ⁡ A → ∃ y y = u | ∃ z ∈ x u = z → ∃ y y ⊆ B ∧ x = ⋃ y
46 31 45 mpd ⊢ C ⊆ B ∧ x ⊆ A ∧ B ∈ TopOn ⁡ A → ∃ y y ⊆ B ∧ x = ⋃ y
47 5 46 syl3an2b ⊢ C ⊆ B ∧ x ∈ 𝒫 A ∧ B ∈ TopOn ⁡ A → ∃ y y ⊆ B ∧ x = ⋃ y
48 47 3com23 ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A ∧ x ∈ 𝒫 A → ∃ y y ⊆ B ∧ x = ⋃ y
49 48 3expia ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → x ∈ 𝒫 A → ∃ y y ⊆ B ∧ x = ⋃ y
50 topontop ⊢ B ∈ TopOn ⁡ A → B ∈ Top
51 tgtop ⊢ B ∈ Top → topGen ⁡ B = B
52 50 51 syl ⊢ B ∈ TopOn ⁡ A → topGen ⁡ B = B
53 52 eleq2d ⊢ B ∈ TopOn ⁡ A → x ∈ topGen ⁡ B ↔ x ∈ B
54 eltg3 ⊢ B ∈ TopOn ⁡ A → x ∈ topGen ⁡ B ↔ ∃ y y ⊆ B ∧ x = ⋃ y
55 53 54 bitr3d ⊢ B ∈ TopOn ⁡ A → x ∈ B ↔ ∃ y y ⊆ B ∧ x = ⋃ y
56 55 adantl ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → x ∈ B ↔ ∃ y y ⊆ B ∧ x = ⋃ y
57 49 56 sylibrd ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → x ∈ 𝒫 A → x ∈ B
58 57 ssrdv ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → 𝒫 A ⊆ B
59 4 58 eqssd ⊢ C ⊆ B ∧ B ∈ TopOn ⁡ A → B = 𝒫 A