fneval

Description: Two covers are finer than each other iff they are both bases for the same topology. (Contributed by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypothesis	fneval.1	⊢ ∼ = ( Fne ∩ ^◡ Fne )
	Assertion	fneval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∼ 𝐵 ↔ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fneval.1	⊢ ∼ = ( Fne ∩ ^◡ Fne )
2	1	breqi	⊢ ( 𝐴 ∼ 𝐵 ↔ 𝐴 ( Fne ∩ ^◡ Fne ) 𝐵 )
3		brin	⊢ ( 𝐴 ( Fne ∩ ^◡ Fne ) 𝐵 ↔ ( 𝐴 Fne 𝐵 ∧ 𝐴 ^◡ Fne 𝐵 ) )
4		fnerel	⊢ Rel Fne
5	4	relbrcnv	⊢ ( 𝐴 ^◡ Fne 𝐵 ↔ 𝐵 Fne 𝐴 )
6	5	anbi2i	⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐴 ^◡ Fne 𝐵 ) ↔ ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) )
7	3 6	bitri	⊢ ( 𝐴 ( Fne ∩ ^◡ Fne ) 𝐵 ↔ ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) )
8	2 7	bitri	⊢ ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) )
9		eqid	⊢ ∪ 𝐴 = ∪ 𝐴
10		eqid	⊢ ∪ 𝐵 = ∪ 𝐵
11	9 10	isfne4b	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 Fne 𝐵 ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ) )
12	10 9	isfne4b	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 Fne 𝐴 ↔ ( ∪ 𝐵 = ∪ 𝐴 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
13		eqcom	⊢ ( ∪ 𝐵 = ∪ 𝐴 ↔ ∪ 𝐴 = ∪ 𝐵 )
14	13	anbi1i	⊢ ( ( ∪ 𝐵 = ∪ 𝐴 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) )
15	12 14	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 Fne 𝐴 ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
16	11 15	bi2anan9r	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) ↔ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) ) )
17		eqss	⊢ ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ↔ ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) )
18	17	anbi2i	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
19		anandi	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) ↔ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
20	18 19	bitri	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ↔ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
21	16 20	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ) )
22		unieq	⊢ ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) → ∪ ( topGen ‘ 𝐴 ) = ∪ ( topGen ‘ 𝐵 ) )
23		unitg	⊢ ( 𝐴 ∈ 𝑉 → ∪ ( topGen ‘ 𝐴 ) = ∪ 𝐴 )
24		unitg	⊢ ( 𝐵 ∈ 𝑊 → ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 )
25	23 24	eqeqan12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∪ ( topGen ‘ 𝐴 ) = ∪ ( topGen ‘ 𝐵 ) ↔ ∪ 𝐴 = ∪ 𝐵 ) )
26	22 25	syl5ib	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) → ∪ 𝐴 = ∪ 𝐵 ) )
27	26	pm4.71rd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ) )
28	21 27	bitr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) ↔ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) )
29	8 28	syl5bb	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∼ 𝐵 ↔ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) )

Metamath Proof Explorer

Theorem fneval

Proof