Theorem isfne

Description: The predicate " B is finer than A ". This property is, in a sense, the opposite of refinement, as refinement requires every element to be a subset of an element of the original and fineness requires that every element of the original have a subset in the finer cover containing every point. I do not know of a literature reference for this. (Contributed by Jeff Hankins, 28-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		isfne.1	⊢ 𝑋 = ∪ 𝐴
2		isfne.2	⊢ 𝑌 = ∪ 𝐵
3		fnerel	⊢ Rel Fne
4	3	brrelex1i	⊢ ( 𝐴 Fne 𝐵 → 𝐴 ∈ V )
5	4	anim1i	⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) )
6	5	ancoms	⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 Fne 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) )
7		simpr	⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
8	7 1 2	3eqtr3g	⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 = ∪ 𝐵 )
9		simpr	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪ 𝐵 ) → ∪ 𝐴 = ∪ 𝐵 )
10		uniexg	⊢ ( 𝐵 ∈ 𝐶 → ∪ 𝐵 ∈ V )
11	10	adantr	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪ 𝐵 ) → ∪ 𝐵 ∈ V )
12	9 11	eqeltrd	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪ 𝐵 ) → ∪ 𝐴 ∈ V )
13		uniexb	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
14	12 13	sylibr	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪ 𝐵 ) → 𝐴 ∈ V )
15		simpl	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪ 𝐵 ) → 𝐵 ∈ 𝐶 )
16	14 15	jca	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪ 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) )
17	8 16	syldan	⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) )
18	17	adantrr	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) )
19		unieq	⊢ ( 𝑟 = 𝐴 → ∪ 𝑟 = ∪ 𝐴 )
20	19 1	eqtr4di	⊢ ( 𝑟 = 𝐴 → ∪ 𝑟 = 𝑋 )
21	20	eqeq1d	⊢ ( 𝑟 = 𝐴 → ( ∪ 𝑟 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑠 ) )
22		raleq	⊢ ( 𝑟 = 𝐴 → ( ∀ 𝑥 ∈ 𝑟 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ) )
23	21 22	anbi12d	⊢ ( 𝑟 = 𝐴 → ( ( ∪ 𝑟 = ∪ 𝑠 ∧ ∀ 𝑥 ∈ 𝑟 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ) ↔ ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ) ) )
24		unieq	⊢ ( 𝑠 = 𝐵 → ∪ 𝑠 = ∪ 𝐵 )
25	24 2	eqtr4di	⊢ ( 𝑠 = 𝐵 → ∪ 𝑠 = 𝑌 )
26	25	eqeq2d	⊢ ( 𝑠 = 𝐵 → ( 𝑋 = ∪ 𝑠 ↔ 𝑋 = 𝑌 ) )
27		ineq1	⊢ ( 𝑠 = 𝐵 → ( 𝑠 ∩ 𝒫 𝑥 ) = ( 𝐵 ∩ 𝒫 𝑥 ) )
28	27	unieqd	⊢ ( 𝑠 = 𝐵 → ∪ ( 𝑠 ∩ 𝒫 𝑥 ) = ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
29	28	sseq2d	⊢ ( 𝑠 = 𝐵 → ( 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
30	29	ralbidv	⊢ ( 𝑠 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
31	26 30	anbi12d	⊢ ( 𝑠 = 𝐵 → ( ( 𝑋 = ∪ 𝑠 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )
32		df-fne	⊢ Fne = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ∪ 𝑟 = ∪ 𝑠 ∧ ∀ 𝑥 ∈ 𝑟 𝑥 ⊆ ∪ ( 𝑠 ∩ 𝒫 𝑥 ) ) }
33	23 31 32	brabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )
34	6 18 33	pm5.21nd	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )