Theorem isfne3

Description: The predicate " B is finer than A ". (Contributed by Jeff Hankins, 11-Oct-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	isfne.1	⊢ 𝑋 = ∪ 𝐴
	isfne.2	⊢ 𝑌 = ∪ 𝐵
Assertion	isfne3	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfne.1	⊢ 𝑋 = ∪ 𝐴
2		isfne.2	⊢ 𝑌 = ∪ 𝐵
3	1 2	isfne4	⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
4		dfss3	⊢ ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) )
5		eltg3	⊢ ( 𝐵 ∈ 𝐶 → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) )
6	5	ralbidv	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) )
7	4 6	bitrid	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) )
8	7	anbi2d	⊢ ( 𝐵 ∈ 𝐶 → ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )
9	3 8	bitrid	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )