Definition df-found 5905

Description: Define the set of all founded relationships over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-found	⊢ Fr = {⟨r, a⟩ ∣ ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))}

Distinct variable group:   r,a,x,y,z

Detailed syntax breakdown of Definition df-found

Step	Hyp	Ref	Expression
1		cfound 5894	. 2 class Fr
2		vx	. . . . . . . 8 setvar x
3	2	cv 1641	. . . . . . 7 class x
4		va	. . . . . . . 8 setvar a
5	4	cv 1641	. . . . . . 7 class a
6	3, 5	wss 3257	. . . . . 6 wff x ⊆ a
7		c0 3550	. . . . . . 7 class ∅
8	3, 7	wne 2516	. . . . . 6 wff x ≠ ∅
9	6, 8	wa 358	. . . . 5 wff (x ⊆ a ∧ x ≠ ∅)
10		vy	. . . . . . . . . 10 setvar y
11	10	cv 1641	. . . . . . . . 9 class y
12		vz	. . . . . . . . . 10 setvar z
13	12	cv 1641	. . . . . . . . 9 class z
14		vr	. . . . . . . . . 10 setvar r
15	14	cv 1641	. . . . . . . . 9 class r
16	11, 13, 15	wbr 4639	. . . . . . . 8 wff yrz
17	10, 12	weq 1643	. . . . . . . 8 wff y = z
18	16, 17	wi 4	. . . . . . 7 wff (yrz → y = z)
19	18, 10, 3	wral 2614	. . . . . 6 wff ∀y ∈ x (yrz → y = z)
20	19, 12, 3	wrex 2615	. . . . 5 wff ∃z ∈ x ∀y ∈ x (yrz → y = z)
21	9, 20	wi 4	. . . 4 wff ((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))
22	21, 2	wal 1540	. . 3 wff ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))
23	22, 14, 4	copab 4622	. 2 class {⟨r, a⟩ ∣ ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))}
24	1, 23	wceq 1642	1 wff Fr = {⟨r, a⟩ ∣ ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))}

This definition is referenced by:  foundex  5914  frd  5922