Definition df-ref 23513

Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.)

Assertion

Ref	Expression
df-ref	⊢ Ref = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)}

Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-ref

Step	Hyp	Ref	Expression
1		cref 23510	. 2 class Ref
2		vy	. . . . . . 7 setvar 𝑦
3	2	cv 1539	. . . . . 6 class 𝑦
4	3	cuni 4907	. . . . 5 class ∪ 𝑦
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1539	. . . . . 6 class 𝑥
7	6	cuni 4907	. . . . 5 class ∪ 𝑥
8	4, 7	wceq 1540	. . . 4 wff ∪ 𝑦 = ∪ 𝑥
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1539	. . . . . . 7 class 𝑧
11		vw	. . . . . . . 8 setvar 𝑤
12	11	cv 1539	. . . . . . 7 class 𝑤
13	10, 12	wss 3951	. . . . . 6 wff 𝑧 ⊆ 𝑤
14	13, 11, 3	wrex 3070	. . . . 5 wff ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤
15	14, 9, 6	wral 3061	. . . 4 wff ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤
16	8, 15	wa 395	. . 3 wff (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)
17	16, 5, 2	copab 5205	. 2 class {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)}
18	1, 17	wceq 1540	1 wff Ref = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)}

This definition is referenced by:  refrel  23516  isref  23517