Theorem eltg2

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	eltg2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgval2	⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } )
2	1	eleq2d	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ) )
3		elex	⊢ ( 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } → 𝐴 ∈ V )
4	3	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ) → 𝐴 ∈ V )
5		uniexg	⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V )
6		ssexg	⊢ ( ( 𝐴 ⊆ ∪ 𝐵 ∧ ∪ 𝐵 ∈ V ) → 𝐴 ∈ V )
7	5 6	sylan2	⊢ ( ( 𝐴 ⊆ ∪ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
8	7	ancoms	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝐵 ) → 𝐴 ∈ V )
9	8	adantrr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) → 𝐴 ∈ V )
10		sseq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ⊆ ∪ 𝐵 ↔ 𝐴 ⊆ ∪ 𝐵 ) )
11		sseq2	⊢ ( 𝑧 = 𝐴 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝐴 ) )
12	11	anbi2d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )
13	12	rexbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )
14	13	raleqbi1dv	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )
15	10 14	anbi12d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) )
16	15	elabg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) )
17	4 9 16	pm5.21nd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) )
18	2 17	bitrd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) )