Metamath Proof Explorer

Definition df-mfrel

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

Ref Expression
Assertion df-mfrel ⊢ mFRel = t ∈ V ⟼ r ∈ 𝒫 mUV ⁡ t × mUV ⁡ t | r -1 = r ∧ ∀ c ∈ mVT ⁡ t ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfr class mFRel
1 vt setvar t
2 cvv class V
3 vr setvar r
4 cmuv class mUV
5 1 cv setvar t
6 5 4 cfv class mUV ⁡ t
7 6 6 cxp class mUV ⁡ t × mUV ⁡ t
8 7 cpw class 𝒫 mUV ⁡ t × mUV ⁡ t
9 3 cv setvar r
10 9 ccnv class r -1
11 10 9 wceq wff r -1 = r
12 vc setvar c
13 cmvt class mVT
14 5 13 cfv class mVT ⁡ t
15 vw setvar w
16 6 cpw class 𝒫 mUV ⁡ t
17 cfn class Fin
18 16 17 cin class 𝒫 mUV ⁡ t ∩ Fin
19 vv setvar v
20 12 cv setvar c
21 20 csn class c
22 6 21 cima class mUV ⁡ t c
23 15 cv setvar w
24 19 cv setvar v
25 24 csn class v
26 9 25 cima class r v
27 23 26 wss wff w ⊆ r v
28 27 19 22 wrex wff ∃ v ∈ mUV ⁡ t c w ⊆ r v
29 28 15 18 wral wff ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v
30 29 12 14 wral wff ∀ c ∈ mVT ⁡ t ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v
31 11 30 wa wff r -1 = r ∧ ∀ c ∈ mVT ⁡ t ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v
32 31 3 8 crab class r ∈ 𝒫 mUV ⁡ t × mUV ⁡ t | r -1 = r ∧ ∀ c ∈ mVT ⁡ t ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v
33 1 2 32 cmpt class t ∈ V ⟼ r ∈ 𝒫 mUV ⁡ t × mUV ⁡ t | r -1 = r ∧ ∀ c ∈ mVT ⁡ t ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v
34 0 33 wceq wff mFRel = t ∈ V ⟼ r ∈ 𝒫 mUV ⁡ t × mUV ⁡ t | r -1 = r ∧ ∀ c ∈ mVT ⁡ t ∀ w ∈ 𝒫 mUV ⁡ t ∩ Fin ∃ v ∈ mUV ⁡ t c w ⊆ r v