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	⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
Assertion	dissneqlem	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ ( TopOn ‘ 𝐴 ) ) → 𝐵 = 𝒫 𝐴 )

Proof

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