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 𝐵 )