Theorem isfne4b

Description: A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		isfne.1	⊢ 𝑋 = ∪ 𝐴
2		isfne.2	⊢ 𝑌 = ∪ 𝐵
3	1 2	isfne4	⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
4		simpr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
5	4 1 2	3eqtr3g	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 = ∪ 𝐵 )
6		uniexg	⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V )
7	6	adantr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ∪ 𝐵 ∈ V )
8	5 7	eqeltrd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 ∈ V )
9		uniexb	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
10	8 9	sylibr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → 𝐴 ∈ V )
11		simpl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → 𝐵 ∈ 𝑉 )
12		tgss3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
13	10 11 12	syl2anc	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
14	13	pm5.32da	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑋 = 𝑌 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ) )
15	3 14	bitr4id	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ) )