Definition df-mfrel 33483

Description: Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-mfrel	⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))})

Distinct variable group:   𝑟,𝑐,𝑡,𝑣,𝑤

Detailed syntax breakdown of Definition df-mfrel

Step	Hyp	Ref	Expression
1		cmfr 33471	. 2 class mFRel
2		vt	. . 3 setvar 𝑡
3		cvv 3422	. . 3 class V
4		vr	. . . . . . . 8 setvar 𝑟
5	4	cv 1538	. . . . . . 7 class 𝑟
6	5	ccnv 5579	. . . . . 6 class ◡𝑟
7	6, 5	wceq 1539	. . . . 5 wff ◡𝑟 = 𝑟
8		vw	. . . . . . . . . 10 setvar 𝑤
9	8	cv 1538	. . . . . . . . 9 class 𝑤
10		vv	. . . . . . . . . . . 12 setvar 𝑣
11	10	cv 1538	. . . . . . . . . . 11 class 𝑣
12	11	csn 4558	. . . . . . . . . 10 class {𝑣}
13	5, 12	cima 5583	. . . . . . . . 9 class (𝑟 “ {𝑣})
14	9, 13	wss 3883	. . . . . . . 8 wff 𝑤 ⊆ (𝑟 “ {𝑣})
15	2	cv 1538	. . . . . . . . . 10 class 𝑡
16		cmuv 33467	. . . . . . . . . 10 class mUV
17	15, 16	cfv 6418	. . . . . . . . 9 class (mUV‘𝑡)
18		vc	. . . . . . . . . . 11 setvar 𝑐
19	18	cv 1538	. . . . . . . . . 10 class 𝑐
20	19	csn 4558	. . . . . . . . 9 class {𝑐}
21	17, 20	cima 5583	. . . . . . . 8 class ((mUV‘𝑡) “ {𝑐})
22	14, 10, 21	wrex 3064	. . . . . . 7 wff ∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣})
23	17	cpw 4530	. . . . . . . 8 class 𝒫 (mUV‘𝑡)
24		cfn 8691	. . . . . . . 8 class Fin
25	23, 24	cin 3882	. . . . . . 7 class (𝒫 (mUV‘𝑡) ∩ Fin)
26	22, 8, 25	wral 3063	. . . . . 6 wff ∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣})
27		cmvt 33325	. . . . . . 7 class mVT
28	15, 27	cfv 6418	. . . . . 6 class (mVT‘𝑡)
29	26, 18, 28	wral 3063	. . . . 5 wff ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣})
30	7, 29	wa 395	. . . 4 wff (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))
31	17, 17	cxp 5578	. . . . 5 class ((mUV‘𝑡) × (mUV‘𝑡))
32	31	cpw 4530	. . . 4 class 𝒫 ((mUV‘𝑡) × (mUV‘𝑡))
33	30, 4, 32	crab 3067	. . 3 class {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))}
34	2, 3, 33	cmpt 5153	. 2 class (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))})
35	1, 34	wceq 1539	1 wff mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))})

This definition is referenced by: (None)