Theorem isfne4

Description: The predicate " B is finer than A " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	isfne.1	⊢ 𝑋 = ∪ 𝐴
	isfne.2	⊢ 𝑌 = ∪ 𝐵
Assertion	isfne4	⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfne.1	⊢ 𝑋 = ∪ 𝐴
2		isfne.2	⊢ 𝑌 = ∪ 𝐵
3		fnerel	⊢ Rel Fne
4	3	brrelex2i	⊢ ( 𝐴 Fne 𝐵 → 𝐵 ∈ V )
5		simpl	⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → 𝑋 = 𝑌 )
6	5 1 2	3eqtr3g	⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝐴 = ∪ 𝐵 )
7		fvex	⊢ ( topGen ‘ 𝐵 ) ∈ V
8	7	ssex	⊢ ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) → 𝐴 ∈ V )
9	8	adantl	⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐴 ∈ V )
10	9	uniexd	⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝐴 ∈ V )
11	6 10	eqeltrrd	⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝐵 ∈ V )
12		uniexb	⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
13	11 12	sylibr	⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐵 ∈ V )
14	1 2	isfne	⊢ ( 𝐵 ∈ V → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )
15		dfss3	⊢ ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) )
16		eltg	⊢ ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
17	16	ralbidv	⊢ ( 𝐵 ∈ V → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
18	15 17	bitrid	⊢ ( 𝐵 ∈ V → ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
19	18	anbi2d	⊢ ( 𝐵 ∈ V → ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )
20	14 19	bitr4d	⊢ ( 𝐵 ∈ V → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ) )
21	4 13 20	pm5.21nii	⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )