Definition df-ref 22115

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 22112	. 2 class Ref
2		vy	. . . . . . 7 setvar 𝑦
3	2	cv 1536	. . . . . 6 class 𝑦
4	3	cuni 4840	. . . . 5 class ∪ 𝑦
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1536	. . . . . 6 class 𝑥
7	6	cuni 4840	. . . . 5 class ∪ 𝑥
8	4, 7	wceq 1537	. . . 4 wff ∪ 𝑦 = ∪ 𝑥
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1536	. . . . . . 7 class 𝑧
11		vw	. . . . . . . 8 setvar 𝑤
12	11	cv 1536	. . . . . . 7 class 𝑤
13	10, 12	wss 3938	. . . . . 6 wff 𝑧 ⊆ 𝑤
14	13, 11, 3	wrex 3141	. . . . 5 wff ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤
15	14, 9, 6	wral 3140	. . . 4 wff ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤
16	8, 15	wa 398	. . 3 wff (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)
17	16, 5, 2	copab 5130	. 2 class {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)}
18	1, 17	wceq 1537	1 wff Ref = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)}

This definition is referenced by:  refrel  22118  isref  22119