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

Metamath Proof Explorer

Theorem fness

Description: A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009)

Ref Expression
Hypotheses fness.1 ⊢ 𝑋 = ∪ 𝐴
fness.2 ⊢ 𝑌 = ∪ 𝐵
Assertion fness ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 Fne 𝐵 )

Proof

Step Hyp Ref Expression
1 fness.1 ⊢ 𝑋 = ∪ 𝐴
2 fness.2 ⊢ 𝑌 = ∪ 𝐵
3 simp3 ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
4 ssel2 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
5 4 3adant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝐵 )
6 simp3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
7 ssid ⊢ 𝑥 ⊆ 𝑥
8 6 7 jctir ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑥 ) )
9 elequ2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑥 ) )
10 sseq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ⊆ 𝑥 ↔ 𝑥 ⊆ 𝑥 ) )
11 9 10 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑥 ) ) )
12 11 rspcev ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
13 5 8 12 syl2anc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
14 13 3expib ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
15 14 ralrimivv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
16 15 3ad2ant2 ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
17 1 2 isfne2 ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) )
18 17 3ad2ant1 ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) )
19 3 16 18 mpbir2and ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 Fne 𝐵 )