Theorem isref 23739

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 36960. 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.)

Hypotheses

Ref	Expression
isref.1	⊢ 𝑋 = ∪ 𝐴
isref.2	⊢ 𝑌 = ∪ 𝐵

Assertion

Ref	Expression
isref	⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵

Allowed substitution hints:   𝐴(𝑦)   𝐶(𝑥, 𝑦)   𝑋(𝑥, 𝑦)   𝑌(𝑥, 𝑦)

Proof of Theorem isref

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		refrel 23738	. . . 4 ⊢ Rel Ref
2	1	brrelex2i 5716	. . 3 ⊢ (𝐴Ref𝐵 → 𝐵 ∈ V)
3	2	anim2i 629	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴Ref𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
4		simpl 488	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐴 ∈ 𝐶)
5		simpr 490	. . . . . . 7 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑋)
6		isref.2	. . . . . . 7 ⊢ 𝑌 = ∪ 𝐵
7		isref.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐴
8	5, 6, 7	3eqtr3g 2820	. . . . . 6 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 = ∪ 𝐴)
9		uniexg 7745	. . . . . . 7 ⊢ (𝐴 ∈ 𝐶 → ∪ 𝐴 ∈ V)
10	9	adantr 486	. . . . . 6 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐴 ∈ V)
11	8, 10	eqeltrd 2862	. . . . 5 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 ∈ V)
12		uniexb 7766	. . . . 5 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V)
13	11, 12	sylibr 237	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝐵 ∈ V)
14	13	adantrr 730	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐵 ∈ V)
15	4, 14	jca 521	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
16		unieq 4881	. . . . . 6 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴)
17	16, 7	eqtr4di 2815	. . . . 5 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = 𝑋)
18	17	eqeq2d 2773	. . . 4 ⊢ (𝑎 = 𝐴 → (∪ 𝑏 = ∪ 𝑎 ↔ ∪ 𝑏 = 𝑋))
19		raleq 3318	. . . 4 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦))
20	18, 19	anbi12d 644	. . 3 ⊢ (𝑎 = 𝐴 → ((∪ 𝑏 = ∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)))
21		unieq 4881	. . . . . 6 ⊢ (𝑏 = 𝐵 → ∪ 𝑏 = ∪ 𝐵)
22	21, 6	eqtr4di 2815	. . . . 5 ⊢ (𝑏 = 𝐵 → ∪ 𝑏 = 𝑌)
23	22	eqeq1d 2764	. . . 4 ⊢ (𝑏 = 𝐵 → (∪ 𝑏 = 𝑋 ↔ 𝑌 = 𝑋))
24		rexeq 3317	. . . . 5 ⊢ (𝑏 = 𝐵 → (∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))
25	24	ralbidv 3187	. . . 4 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))
26	23, 25	anbi12d 644	. . 3 ⊢ (𝑏 = 𝐵 → ((∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)))
27		df-ref 23735	. . 3 ⊢ Ref = {⟨𝑎, 𝑏⟩ ∣ (∪ 𝑏 = ∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)}
28	20, 26, 27	brabg 5522	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)))
29	3, 15, 28	pm5.21nd 814	1 ⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ⊆ wss 3902  ∪ cuni 4870   class class class wbr 5107  Refcref 23732

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-ref 23735

This theorem is used by:  refbas  23740  refssex  23741  ssref  23742  refref  23743  reftr  23744  refun0  23745  dissnref  23758  reff  34351  locfinreflem  34352  cmpcref  34362  fnessref  36978  refssfne  36979