Theorem isref

Description: The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne . On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		isref.1	⊢ 𝑋 = ∪ 𝐴
2		isref.2	⊢ 𝑌 = ∪ 𝐵
3		refrel	⊢ Rel Ref
4	3	brrelex2i	⊢ ( 𝐴 Ref 𝐵 → 𝐵 ∈ V )
5	4	anim2i	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 Ref 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) )
6		simpl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) → 𝐴 ∈ 𝐶 )
7		simpr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋 ) → 𝑌 = 𝑋 )
8	7 2 1	3eqtr3g	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋 ) → ∪ 𝐵 = ∪ 𝐴 )
9		uniexg	⊢ ( 𝐴 ∈ 𝐶 → ∪ 𝐴 ∈ V )
10	9	adantr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋 ) → ∪ 𝐴 ∈ V )
11	8 10	eqeltrd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋 ) → ∪ 𝐵 ∈ V )
12		uniexb	⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
13	11 12	sylibr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋 ) → 𝐵 ∈ V )
14	13	adantrr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) → 𝐵 ∈ V )
15	6 14	jca	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) )
16		unieq	⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴 )
17	16 1	eqtr4di	⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = 𝑋 )
18	17	eqeq2d	⊢ ( 𝑎 = 𝐴 → ( ∪ 𝑏 = ∪ 𝑎 ↔ ∪ 𝑏 = 𝑋 ) )
19		raleq	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ) )
20	18 19	anbi12d	⊢ ( 𝑎 = 𝐴 → ( ( ∪ 𝑏 = ∪ 𝑎 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ) ↔ ( ∪ 𝑏 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ) ) )
21		unieq	⊢ ( 𝑏 = 𝐵 → ∪ 𝑏 = ∪ 𝐵 )
22	21 2	eqtr4di	⊢ ( 𝑏 = 𝐵 → ∪ 𝑏 = 𝑌 )
23	22	eqeq1d	⊢ ( 𝑏 = 𝐵 → ( ∪ 𝑏 = 𝑋 ↔ 𝑌 = 𝑋 ) )
24		rexeq	⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
25	24	ralbidv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
26	23 25	anbi12d	⊢ ( 𝑏 = 𝐵 → ( ( ∪ 𝑏 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ) ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
27		df-ref	⊢ Ref = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ∪ 𝑏 = ∪ 𝑎 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ) }
28	20 26 27	brabg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
29	5 15 28	pm5.21nd	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )