Definition df-ref

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cref	⊢ Ref
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	2	cv	⊢ 𝑦
4	3	cuni	⊢ ∪ 𝑦
5	1	cv	⊢ 𝑥
6	5	cuni	⊢ ∪ 𝑥
7	4 6	wceq	⊢ ∪ 𝑦 = ∪ 𝑥
8		vz	⊢ 𝑧
9		vw	⊢ 𝑤
10	8	cv	⊢ 𝑧
11	9	cv	⊢ 𝑤
12	10 11	wss	⊢ 𝑧 ⊆ 𝑤
13	12 9 3	wrex	⊢ ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤
14	13 8 5	wral	⊢ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤
15	7 14	wa	⊢ ( ∪ 𝑦 = ∪ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 )
16	15 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑦 = ∪ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) }
17	0 16	wceq	⊢ Ref = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑦 = ∪ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) }