mmdefinitions - New Foundations Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
wn 3	wff ¬ φ
wi 4	wff (φ → ψ)
ax-mp 5	⊢ φ    &   ⊢ (φ → ψ)    ⇒   ⊢ ψ
ax-1 6	⊢ (φ → (ψ → φ))
ax-2 7	⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
ax-3 8	⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
wb 176	wff (φ ↔ ψ)
df-bi 177	⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
wo 357	wff (φ ∨ ψ)
wa 358	wff (φ ∧ ψ)
df-or 359	⊢ ((φ ∨ ψ) ↔ (¬ φ → ψ))
df-an 360	⊢ ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))
w3o 933	wff (φ ∨ ψ ∨ χ)
w3a 934	wff (φ ∧ ψ ∧ χ)
df-3or 935	⊢ ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))
df-3an 936	⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))
wnan 1287	wff (φ ⊼ ψ)
df-nan 1288	⊢ ((φ ⊼ ψ) ↔ ¬ (φ ∧ ψ))
wxo 1304	wff (φ ⊻ ψ)
df-xor 1305	⊢ ((φ ⊻ ψ) ↔ ¬ (φ ↔ ψ))
wtru 1316	wff ⊤
wfal 1317	wff ⊥
df-tru 1319	⊢ ( ⊤ ↔ (φ ↔ φ))
df-fal 1320	⊢ ( ⊥ ↔ ¬ ⊤ )
whad 1378	wff hadd(φ, ψ, χ)
wcad 1379	wff cadd(φ, ψ, χ)
df-had 1380	⊢ (hadd(φ, ψ, χ) ↔ ((φ ⊻ ψ) ⊻ χ))
df-cad 1381	⊢ (cadd(φ, ψ, χ) ↔ ((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ))))
ax-meredith 1406	⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))
wal 1540	wff ∀xφ
wex 1541	wff ∃xφ
df-ex 1542	⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
wnf 1544	wff Ⅎxφ
df-nf 1545	⊢ (Ⅎxφ ↔ ∀x(φ → ∀xφ))
ax-gen 1546	⊢ φ    ⇒   ⊢ ∀xφ
ax-5 1557	⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))
ax-17 1616	⊢ (φ → ∀xφ)
cv 1641	class x
wceq 1642	wff A = B
wsb 1648	wff [y / x]φ
df-sb 1649	⊢ ([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ)))
ax-9 1654	⊢ ¬ ∀x ¬ x = y
ax-8 1675	⊢ (x = y → (x = z → y = z))
wcel 1710	wff A ∈ B
ax-13 1712	⊢ (x = y → (x ∈ z → y ∈ z))
ax-14 1714	⊢ (x = y → (z ∈ x → z ∈ y))
ax-6 1729	⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)
ax-7 1734	⊢ (∀x∀yφ → ∀y∀xφ)
ax-11 1746	⊢ (x = y → (∀yφ → ∀x(x = y → φ)))
ax-12 1925	⊢ (¬ x = y → (y = z → ∀x y = z))
ax-4 2135	⊢ (∀xφ → φ)
ax-5o 2136	⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
ax-6o 2137	⊢ (¬ ∀x ¬ ∀xφ → φ)
ax-9o 2138	⊢ (∀x(x = y → ∀xφ) → φ)
ax-10o 2139	⊢ (∀x x = y → (∀xφ → ∀yφ))
ax-10 2140	⊢ (∀x x = y → ∀y y = x)
ax-11o 2141	⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
ax-12o 2142	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
ax-15 2143	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
ax-16 2144	⊢ (∀x x = y → (φ → ∀xφ))
weu 2204	wff ∃!xφ
wmo 2205	wff ∃*xφ
df-eu 2208	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
df-mo 2209	⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))
ax-7d 2295	⊢ (∀x∀yφ → ∀y∀xφ)
ax-8d 2296	⊢ (x = y → (x = z → y = z))
ax-9d1 2297	⊢ ¬ ∀x ¬ x = x
ax-9d2 2298	⊢ ¬ ∀x ¬ x = y
ax-10d 2299	⊢ (∀x x = y → ∀y y = x)
ax-11d 2300	⊢ (x = y → (∀yφ → ∀x(x = y → φ)))
ax-ext 2334	⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
cab 2339	class {x ∣ φ}
df-clab 2340	⊢ (x ∈ {y ∣ φ} ↔ [x / y]φ)
df-cleq 2346	⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z)    ⇒   ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
df-clel 2349	⊢ (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))
wnfc 2476	wff ℲxA
df-nfc 2478	⊢ (ℲxA ↔ ∀yℲx y ∈ A)
wne 2516	wff A ≠ B
wnel 2517	wff A ∉ B
df-ne 2518	⊢ (A ≠ B ↔ ¬ A = B)
df-nel 2519	⊢ (A ∉ B ↔ ¬ A ∈ B)
wral 2614	wff ∀x ∈ A φ
wrex 2615	wff ∃x ∈ A φ
wreu 2616	wff ∃!x ∈ A φ
wrmo 2617	wff ∃*x ∈ A φ
crab 2618	class {x ∈ A ∣ φ}
df-ral 2619	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
df-rex 2620	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
df-reu 2621	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
df-rmo 2622	⊢ (∃*x ∈ A φ ↔ ∃*x(x ∈ A ∧ φ))
df-rab 2623	⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}
cvv 2859	class V
df-v 2861	⊢ V = {x ∣ x = x}
wsbc 3046	wff [̣A / x]̣φ
df-sbc 3047	⊢ ([̣A / x]̣φ ↔ A ∈ {x ∣ φ})
csb 3136	class [A / x]B
df-csb 3137	⊢ [A / x]B = {y ∣ [̣A / x]̣y ∈ B}
cnin 3204	class (A ⩃ B)
ccompl 3205	class ∼ A
cdif 3206	class (A ∖ B)
cun 3207	class (A ∪ B)
cin 3208	class (A ∩ B)
csymdif 3209	class (A ⊕ B)
df-nin 3211	⊢ (A ⩃ B) = {x ∣ (x ∈ A ⊼ x ∈ B)}
df-compl 3212	⊢ ∼ A = (A ⩃ A)
df-in 3213	⊢ (A ∩ B) = ∼ (A ⩃ B)
df-un 3214	⊢ (A ∪ B) = ( ∼ A ⩃ ∼ B)
df-dif 3215	⊢ (A ∖ B) = (A ∩ ∼ B)
df-symdif 3216	⊢ (A ⊕ B) = ((A ∖ B) ∪ (B ∖ A))
wss 3257	wff A ⊆ B
wpss 3258	wff A ⊊ B
df-ss 3259	⊢ (A ⊆ B ↔ (A ∩ B) = A)
df-pss 3261	⊢ (A ⊊ B ↔ (A ⊆ B ∧ A ≠ B))
c0 3550	class ∅
df-nul 3551	⊢ ∅ = (V ∖ V)
cif 3662	class if(φ, A, B)
df-if 3663	⊢ if(φ, A, B) = {x ∣ ((x ∈ A ∧ φ) ∨ (x ∈ B ∧ ¬ φ))}
cpw 3722	class ℘A
df-pw 3724	⊢ ℘A = {x ∣ x ⊆ A}
csn 3737	class {A}
cpr 3738	class {A, B}
ctp 3739	class {A, B, C}
df-sn 3741	⊢ {A} = {x ∣ x = A}
df-pr 3742	⊢ {A, B} = ({A} ∪ {B})
df-tp 3743	⊢ {A, B, C} = ({A, B} ∪ {C})
cuni 3891	class ∪A
df-uni 3892	⊢ ∪A = {x ∣ ∃y(x ∈ y ∧ y ∈ A)}
cint 3926	class ∩A
df-int 3927	⊢ ∩A = {x ∣ ∀y(y ∈ A → x ∈ y)}
ciun 3969	class ∪x ∈ A B
ciin 3970	class ∩x ∈ A B
df-iun 3971	⊢ ∪x ∈ A B = {y ∣ ∃x ∈ A y ∈ B}
df-iin 3972	⊢ ∩x ∈ A B = {y ∣ ∀x ∈ A y ∈ B}
copk 4057	class ⟪A, B⟫
df-opk 4058	⊢ ⟪A, B⟫ = {{A}, {A, B}}
ax-nin 4078	⊢ ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y))
ax-xp 4079	⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(z = ⟪w, t⟫ ∧ t ∈ x))
ax-cnv 4080	⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
ax-1c 4081	⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z))
ax-sset 4082	⊢ ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))
ax-si 4083	⊢ ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
ax-ins2 4084	⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
ax-ins3 4085	⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
ax-typlower 4086	⊢ ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x)
ax-sn 4087	⊢ ∃y∀z(z ∈ y ↔ z = x)
cuni1 4133	class ⋃1A
c1c 4134	class 1c
cpw1 4135	class ℘1A
df-1c 4136	⊢ 1c = {x ∣ ∃y x = {y}}
df-pw1 4137	⊢ ℘1A = (℘A ∩ 1c)
df-uni1 4138	⊢ ⋃1A = ∪(A ∩ 1c)
cxpk 4174	class (A ×k B)
ccnvk 4175	class ◡kA
cins2k 4176	class Ins2k A
cins3k 4177	class Ins3k A
cp6 4178	class P6 A
cimak 4179	class (A “k B)
ccomk 4180	class (A ∘k B)
csik 4181	class SIk A
cimagek 4182	class ImagekA
cssetk 4183	class Sk
cidk 4184	class Ik
df-xpk 4185	⊢ (A ×k B) = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))}
df-cnvk 4186	⊢ ◡kA = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)}
df-ins2k 4187	⊢ Ins2k A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, v⟫ ∈ A))}
df-ins3k 4188	⊢ Ins3k A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))}
df-imak 4189	⊢ (A “k B) = {x ∣ ∃y ∈ B ⟪y, x⟫ ∈ A}
df-cok 4190	⊢ (A ∘k B) = (( Ins2k A ∩ Ins3k ◡kB) “k V)
df-p6 4191	⊢ P6 A = {x ∣ (V ×k {{x}}) ⊆ A}
df-sik 4192	⊢ SIk A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))}
df-ssetk 4193	⊢ Sk = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y ⊆ z)}
df-imagek 4194	⊢ ImagekA = ((V ×k V) ∖ (( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A)) “k ℘1℘11c))
df-idk 4195	⊢ Ik = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y = z)}
cio 4337	class (℩xφ)
df-iota 4339	⊢ (℩xφ) = ∪{y ∣ {x ∣ φ} = {y}}
cnnc 4373	class Nn
c0c 4374	class 0c
cplc 4375	class (A +c B)
cfin 4376	class Fin
df-0c 4377	⊢ 0c = {∅}
df-addc 4378	⊢ (A +c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
df-nnc 4379	⊢ Nn = ∩{b ∣ (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)}
df-fin 4380	⊢ Fin = ∪ Nn
clefin 4432	class ≤fin
cltfin 4433	class <fin
cncfin 4434	class Ncfin A
ctfin 4435	class Tfin A
cevenfin 4436	class Evenfin
coddfin 4437	class Oddfin
wsfin 4438	wff Sfin (A, B)
cspfin 4439	class Spfin
df-lefin 4440	⊢ ≤fin = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}
df-ltfin 4441	⊢ <fin = {x ∣ ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))}
df-ncfin 4442	⊢ Ncfin A = (℩x(x ∈ Nn ∧ A ∈ x))
df-tfin 4443	⊢ Tfin M = if(M = ∅, ∅, (℩n(n ∈ Nn ∧ ∃a ∈ M ℘1a ∈ n)))
df-evenfin 4444	⊢ Evenfin = {x ∣ (∃n ∈ Nn x = (n +c n) ∧ x ≠ ∅)}
df-oddfin 4445	⊢ Oddfin = {x ∣ (∃n ∈ Nn x = ((n +c n) +c 1c) ∧ x ≠ ∅)}
df-sfin 4446	⊢ ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)))
df-spfin 4447	⊢ Spfin = ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}
cop 4561	class ⟨A, B⟩
cphi 4562	class Phi A
cproj1 4563	class Proj1 A
cproj2 4564	class Proj2 A
df-phi 4565	⊢ Phi A = {y ∣ ∃x ∈ A y = if(x ∈ Nn , (x +c 1c), x)}
df-op 4566	⊢ ⟨A, B⟩ = ({x ∣ ∃y ∈ A x = Phi y} ∪ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})})
df-proj1 4567	⊢ Proj1 A = {x ∣ Phi x ∈ A}
df-proj2 4568	⊢ Proj2 A = {x ∣ ( Phi x ∪ {0c}) ∈ A}
copab 4622	class {⟨x, y⟩ ∣ φ}
df-opab 4623	⊢ {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}
wbr 4639	wff ARB
df-br 4640	⊢ (ARB ↔ ⟨A, B⟩ ∈ R)
c1st 4717	class 1st
cswap 4718	class Swap
csset 4719	class S
csi 4720	class SI A
ccom 4721	class (A ∘ B)
cima 4722	class (A “ B)
df-1st 4723	⊢ 1st = {⟨x, y⟩ ∣ ∃z x = ⟨y, z⟩}
df-swap 4724	⊢ Swap = {⟨x, y⟩ ∣ ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)}
df-sset 4725	⊢ S = {⟨x, y⟩ ∣ x ⊆ y}
df-co 4726	⊢ (A ∘ B) = {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}
df-ima 4727	⊢ (A “ B) = {x ∣ ∃y ∈ B yAx}
df-si 4728	⊢ SI A = {⟨x, y⟩ ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)}
cep 4762	class E
cid 4763	class I
df-eprel 4764	⊢ E = {⟨x, y⟩ ∣ x ∈ y}
df-id 4767	⊢ I = {⟨x, y⟩ ∣ x = y}
cxp 4770	class (A × B)
ccnv 4771	class ◡A
cdm 4772	class dom A
crn 4773	class ran A
cres 4774	class (A ↾ B)
wfun 4775	wff Fun A
wfn 4776	wff A Fn B
wf 4777	wff F:A–→B
wf1 4778	wff F:A–1-1→B
wfo 4779	wff F:A–onto→B
wf1o 4780	wff F:A–1-1-onto→B
cfv 4781	class (F ‘A)
wiso 4782	wff H Isom R, S (A, B)
c2nd 4783	class 2nd
df-xp 4784	⊢ (A × B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ B)}
df-cnv 4785	⊢ ◡A = {⟨x, y⟩ ∣ yAx}
df-rn 4786	⊢ ran A = (A “ V)
df-dm 4787	⊢ dom A = ran ◡A
df-res 4788	⊢ (A ↾ B) = (A ∩ (B × V))
df-fun 4789	⊢ (Fun A ↔ (A ∘ ◡A) ⊆ I )
df-fn 4790	⊢ (A Fn B ↔ (Fun A ∧ dom A = B))
df-f 4791	⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))
df-f1 4792	⊢ (F:A–1-1→B ↔ (F:A–→B ∧ Fun ◡F))
df-fo 4793	⊢ (F:A–onto→B ↔ (F Fn A ∧ ran F = B))
df-f1o 4794	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))
df-fv 4795	⊢ (F ‘A) = (℩xAFx)
df-iso 4796	⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))
df-2nd 4797	⊢ 2nd = {⟨x, y⟩ ∣ ∃z x = ⟨z, y⟩}
co 5525	class (AFB)
df-ov 5526	⊢ (AFB) = (F ‘⟨A, B⟩)
coprab 5527	class {⟨⟨x, y⟩, z⟩ ∣ φ}
df-oprab 5528	⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
cmpt 5651	class (x ∈ A ↦ B)
df-mpt 5652	⊢ (x ∈ A ↦ B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}
cmpt2 5653	class (x ∈ A, y ∈ B ↦ C)
df-mpt2 5654	⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}
ctxp 5735	class (A ⊗ B)
df-txp 5736	⊢ (A ⊗ B) = ((◡1st ∘ A) ∩ (◡2nd ∘ B))
cpprod 5737	class PProd (A, B)
df-pprod 5738	⊢ PProd (A, B) = ((A ∘ 1st ) ⊗ (B ∘ 2nd ))
cfix 5739	class Fix A
df-fix 5740	⊢ Fix A = ran (A ∩ I )
ccup 5741	class Cup
df-cup 5742	⊢ Cup = (x ∈ V, y ∈ V ↦ (x ∪ y))
cdisj 5743	class Disj
df-disj 5744	⊢ Disj = {⟨x, y⟩ ∣ (x ∩ y) = ∅}
caddcfn 5745	class AddC
df-addcfn 5746	⊢ AddC = (x ∈ V, y ∈ V ↦ (x +c y))
ccompose 5747	class Compose
df-compose 5748	⊢ Compose = (x ∈ V, y ∈ V ↦ (x ∘ y))
cins2 5749	class Ins2 A
df-ins2 5750	⊢ Ins2 A = (V ⊗ A)
cins3 5751	class Ins3 A
df-ins3 5752	⊢ Ins3 A = (A ⊗ V)
cimage 5753	class ImageA
df-image 5754	⊢ ImageA = ∼ (( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A)) “ 1c)
cins4 5755	class Ins4 A
df-ins4 5756	⊢ Ins4 A = (◡(1st ⊗ ((1st ∘ 2nd ) ⊗ ((1st ∘ 2nd ) ∘ 2nd ))) “ A)
csi3 5757	class SI3 A
df-si3 5758	⊢ SI3 A = (( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) “ ℘1A)
cfuns 5759	class Funs
df-funs 5760	⊢ Funs = {f ∣ Fun f}
cfns 5761	class Fns
df-fns 5762	⊢ Fns = {⟨f, a⟩ ∣ f Fn a}
ccross 5763	class Cross
df-cross 5764	⊢ Cross = (x ∈ V, y ∈ V ↦ (x × y))
cpw1fn 5765	class Pw1Fn
df-pw1fn 5766	⊢ Pw1Fn = (x ∈ 1c ↦ ℘1∪x)
cfullfun 5767	class FullFun F
df-fullfun 5768	⊢ FullFun F = ((( I ∘ F) ∖ ( ∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅}))
cdomfn 5769	class Dom
df-domfn 5770	⊢ Dom = (x ∈ V ↦ dom x)
cranfn 5771	class Ran
df-ranfn 5772	⊢ Ran = (x ∈ V ↦ ran x)
cclos1 5872	class Clos1 (A, R)
df-clos1 5873	⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)}
ctrans 5888	class Trans
cref 5889	class Ref
cantisym 5890	class Antisym
cpartial 5891	class Po
cconnex 5892	class Connex
cstrict 5893	class Or
cfound 5894	class Fr
cwe 5895	class We
cext 5896	class Ext
csym 5897	class Sym
cer 5898	class Er
df-trans 5899	⊢ Trans = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)}
df-ref 5900	⊢ Ref = {⟨r, a⟩ ∣ ∀x ∈ a xrx}
df-antisym 5901	⊢ Antisym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)}
df-partial 5902	⊢ Po = (( Ref ∩ Trans ) ∩ Antisym )
df-connex 5903	⊢ Connex = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)}
df-strict 5904	⊢ Or = ( Po ∩ Connex )
df-found 5905	⊢ Fr = {⟨r, a⟩ ∣ ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))}
df-we 5906	⊢ We = ( Or ∩ Fr )
df-ext 5907	⊢ Ext = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)}
df-sym 5908	⊢ Sym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry → yrx)}
df-er 5909	⊢ Er = ( Sym ∩ Trans )
cec 5945	class [A]R
cqs 5946	class (A / R)
df-ec 5947	⊢ [A]R = (R “ {A})
df-qs 5951	⊢ (A / R) = {y ∣ ∃x ∈ A y = [x]R}
cmap 5999	class ↑m
cpm 6000	class ↑pm
df-map 6001	⊢ ↑m = (x ∈ V, y ∈ V ↦ {f ∣ f:y–→x})
df-pm 6002	⊢ ↑pm = (x ∈ V, y ∈ V ↦ {f ∈ ℘(y × x) ∣ Fun f})
cen 6028	class ≈
df-en 6029	⊢ ≈ = {⟨x, y⟩ ∣ ∃f f:x–1-1-onto→y}
cncs 6088	class NC
clec 6089	class ≤c
cltc 6090	class <c
cnc 6091	class Nc A
cmuc 6092	class ·c
ctc 6093	class Tc A
c2c 6094	class 2c
c3c 6095	class 3c
cce 6096	class ↑c
ctcfn 6097	class TcFn
df-ncs 6098	⊢ NC = (V / ≈ )
df-lec 6099	⊢ ≤c = {⟨a, b⟩ ∣ ∃x ∈ a ∃y ∈ b x ⊆ y}
df-ltc 6100	⊢ <c = ( ≤c ∖ I )
df-nc 6101	⊢ Nc A = [A] ≈
df-muc 6102	⊢ ·c = (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)})
df-tc 6103	⊢ Tc A = (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc ℘1x))
df-2c 6104	⊢ 2c = Nc {∅, V}
df-3c 6105	⊢ 3c = Nc {∅, V, (V ∖ {∅})}
df-ce 6106	⊢ ↑c = (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))})
df-tcfn 6107	⊢ TcFn = (x ∈ 1c ↦ Tc ∪x)
cspac 6273	class Spac
df-spac 6274	⊢ Spac = (m ∈ NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
cfrec 6309	class FRec (F, I)
df-frec 6310	⊢ FRec (F, I) = Clos1 ({⟨0c, I⟩}, PProd ((x ∈ V ↦ (x +c 1c)), F))
ccan 6323	class Can
df-can 6324	⊢ Can = {x ∣ ℘1x ≈ x}
cscan 6325	class SCan
df-scan 6326	⊢ SCan = {x ∣ (y ∈ x ↦ {y}) ∈ V}