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 \| \exists x \in A u = \{x\}\}$
	Assertion	dissneqlem	$⊢ (C \subseteq B \land B \in TopOn (A)) \to B = 𝒫 A$

Proof

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

Metamath Proof Explorer

Theorem dissneqlem

Proof