Theorem pptbas

Description: The particular point topology is generated by a basis consisting of pairs { x , P } for each x e. A . (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	pptbas	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 ∨ 𝑥 = ∅ ) } = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ppttop	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )
2		topontop	⊢ ( { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) → { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∈ Top )
3	1 2	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∈ Top )
4		eleq2	⊢ ( 𝑦 = { 𝑥 , 𝑃 } → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ { 𝑥 , 𝑃 } ) )
5		eqeq1	⊢ ( 𝑦 = { 𝑥 , 𝑃 } → ( 𝑦 = ∅ ↔ { 𝑥 , 𝑃 } = ∅ ) )
6	4 5	orbi12d	⊢ ( 𝑦 = { 𝑥 , 𝑃 } → ( ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) ↔ ( 𝑃 ∈ { 𝑥 , 𝑃 } ∨ { 𝑥 , 𝑃 } = ∅ ) ) )
7		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
8		simplr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
9	7 8	prssd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 , 𝑃 } ⊆ 𝐴 )
10		prex	⊢ { 𝑥 , 𝑃 } ∈ V
11	10	elpw	⊢ ( { 𝑥 , 𝑃 } ∈ 𝒫 𝐴 ↔ { 𝑥 , 𝑃 } ⊆ 𝐴 )
12	9 11	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 , 𝑃 } ∈ 𝒫 𝐴 )
13		prid2g	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ { 𝑥 , 𝑃 } )
14	13	ad2antlr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑃 ∈ { 𝑥 , 𝑃 } )
15	14	orcd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑃 ∈ { 𝑥 , 𝑃 } ∨ { 𝑥 , 𝑃 } = ∅ ) )
16	6 12 15	elrabd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 , 𝑃 } ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } )
17	16	fmpttd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) : 𝐴 ⟶ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } )
18	17	frnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ⊆ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } )
19		eleq2	⊢ ( 𝑦 = 𝑧 → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑧 ) )
20		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ∅ ↔ 𝑧 = ∅ ) )
21	19 20	orbi12d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) ↔ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) )
22	21	elrab	⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ↔ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) )
23		elpwi	⊢ ( 𝑧 ∈ 𝒫 𝐴 → 𝑧 ⊆ 𝐴 )
24	23	ad2antrl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) → 𝑧 ⊆ 𝐴 )
25	24	sselda	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → 𝑤 ∈ 𝐴 )
26		prid1g	⊢ ( 𝑤 ∈ 𝑧 → 𝑤 ∈ { 𝑤 , 𝑃 } )
27	26	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → 𝑤 ∈ { 𝑤 , 𝑃 } )
28		simpr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → 𝑤 ∈ 𝑧 )
29		n0i	⊢ ( 𝑤 ∈ 𝑧 → ¬ 𝑧 = ∅ )
30	29	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → ¬ 𝑧 = ∅ )
31		simplrr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) )
32	31	ord	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → ( ¬ 𝑃 ∈ 𝑧 → 𝑧 = ∅ ) )
33	30 32	mt3d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → 𝑃 ∈ 𝑧 )
34	28 33	prssd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → { 𝑤 , 𝑃 } ⊆ 𝑧 )
35		preq1	⊢ ( 𝑥 = 𝑤 → { 𝑥 , 𝑃 } = { 𝑤 , 𝑃 } )
36	35	eleq2d	⊢ ( 𝑥 = 𝑤 → ( 𝑤 ∈ { 𝑥 , 𝑃 } ↔ 𝑤 ∈ { 𝑤 , 𝑃 } ) )
37	35	sseq1d	⊢ ( 𝑥 = 𝑤 → ( { 𝑥 , 𝑃 } ⊆ 𝑧 ↔ { 𝑤 , 𝑃 } ⊆ 𝑧 ) )
38	36 37	anbi12d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑤 ∈ { 𝑥 , 𝑃 } ∧ { 𝑥 , 𝑃 } ⊆ 𝑧 ) ↔ ( 𝑤 ∈ { 𝑤 , 𝑃 } ∧ { 𝑤 , 𝑃 } ⊆ 𝑧 ) ) )
39	38	rspcev	⊢ ( ( 𝑤 ∈ 𝐴 ∧ ( 𝑤 ∈ { 𝑤 , 𝑃 } ∧ { 𝑤 , 𝑃 } ⊆ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ { 𝑥 , 𝑃 } ∧ { 𝑥 , 𝑃 } ⊆ 𝑧 ) )
40	25 27 34 39	syl12anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ { 𝑥 , 𝑃 } ∧ { 𝑥 , 𝑃 } ⊆ 𝑧 ) )
41	10	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 { 𝑥 , 𝑃 } ∈ V
42		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } )
43		eleq2	⊢ ( 𝑣 = { 𝑥 , 𝑃 } → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ { 𝑥 , 𝑃 } ) )
44		sseq1	⊢ ( 𝑣 = { 𝑥 , 𝑃 } → ( 𝑣 ⊆ 𝑧 ↔ { 𝑥 , 𝑃 } ⊆ 𝑧 ) )
45	43 44	anbi12d	⊢ ( 𝑣 = { 𝑥 , 𝑃 } → ( ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ↔ ( 𝑤 ∈ { 𝑥 , 𝑃 } ∧ { 𝑥 , 𝑃 } ⊆ 𝑧 ) ) )
46	42 45	rexrnmptw	⊢ ( ∀ 𝑥 ∈ 𝐴 { 𝑥 , 𝑃 } ∈ V → ( ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ { 𝑥 , 𝑃 } ∧ { 𝑥 , 𝑃 } ⊆ 𝑧 ) ) )
47	41 46	ax-mp	⊢ ( ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ { 𝑥 , 𝑃 } ∧ { 𝑥 , 𝑃 } ⊆ 𝑧 ) )
48	40 47	sylibr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) ∧ 𝑤 ∈ 𝑧 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) )
49	48	ralrimiva	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) ) → ∀ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) )
50	49	ex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 ∨ 𝑧 = ∅ ) ) → ∀ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) )
51	22 50	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } → ∀ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) )
52	51	ralrimiv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ∀ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∀ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) )
53		basgen2	⊢ ( ( { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∈ Top ∧ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ⊆ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∧ ∀ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } ∀ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ( 𝑤 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ) = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } )
54	3 18 52 53	syl3anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( topGen ‘ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ) = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } )
55		eleq2	⊢ ( 𝑦 = 𝑥 → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑥 ) )
56		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ∅ ↔ 𝑥 = ∅ ) )
57	55 56	orbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) ↔ ( 𝑃 ∈ 𝑥 ∨ 𝑥 = ∅ ) ) )
58	57	cbvrabv	⊢ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑦 ∨ 𝑦 = ∅ ) } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 ∨ 𝑥 = ∅ ) }
59	54 58	eqtr2di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 ∨ 𝑥 = ∅ ) } = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ) )