This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )