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 2477	wff ℲxA
df-nfc 2479	⊢ (ℲxA ↔ ∀yℲx y ∈ A)
wne 2517	wff A ≠ B
wnel 2518	wff A ∉ B
df-ne 2519	⊢ (A ≠ B ↔ ¬ A = B)
df-nel 2520	⊢ (A ∉ B ↔ ¬ A ∈ B)
wral 2615	wff ∀x ∈ A φ
wrex 2616	wff ∃x ∈ A φ
wreu 2617	wff ∃!x ∈ A φ
wrmo 2618	wff ∃*x ∈ A φ
crab 2619	class {x ∈ A ∣ φ}
df-ral 2620	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
df-rex 2621	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
df-reu 2622	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
df-rmo 2623	⊢ (∃*x ∈ A φ ↔ ∃*x(x ∈ A ∧ φ))
df-rab 2624	⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}
cvv 2860	class V
df-v 2862	⊢ V = {x ∣ x = x}
wsbc 3047	wff [̣A / x]̣φ
df-sbc 3048	⊢ ([̣A / x]̣φ ↔ A ∈ {x ∣ φ})
csb 3137	class [A / x]B
df-csb 3138	⊢ [A / x]B = {y ∣ [̣A / x]̣y ∈ B}
cnin 3205	class (A ⩃ B)
ccompl 3206	class ∼ A
cdif 3207	class (A ∖ B)
cun 3208	class (A ∪ B)
cin 3209	class (A ∩ B)
csymdif 3210	class (A ⊕ B)
df-nin 3212	⊢ (A ⩃ B) = {x ∣ (x ∈ A ⊼ x ∈ B)}
df-compl 3213	⊢ ∼ A = (A ⩃ A)
df-in 3214	⊢ (A ∩ B) = ∼ (A ⩃ B)
df-un 3215	⊢ (A ∪ B) = ( ∼ A ⩃ ∼ B)
df-dif 3216	⊢ (A ∖ B) = (A ∩ ∼ B)
df-symdif 3217	⊢ (A ⊕ B) = ((A ∖ B) ∪ (B ∖ A))
wss 3258	wff A ⊆ B
wpss 3259	wff A ⊊ B
df-ss 3260	⊢ (A ⊆ B ↔ (A ∩ B) = A)
df-pss 3262	⊢ (A ⊊ B ↔ (A ⊆ B ∧ A ≠ B))
c0 3551	class ∅
df-nul 3552	⊢ ∅ = (V ∖ V)
cif 3663	class if(φ, A, B)
df-if 3664	⊢ if(φ, A, B) = {x ∣ ((x ∈ A ∧ φ) ∨ (x ∈ B ∧ ¬ φ))}
cpw 3723	class 𝒫 A
df-pw 3725	⊢ 𝒫 A = {x ∣ x ⊆ A}
csn 3738	class {A}
cpr 3739	class {A, B}
ctp 3740	class {A, B, C}
df-sn 3742	⊢ {A} = {x ∣ x = A}
df-pr 3743	⊢ {A, B} = ({A} ∪ {B})
df-tp 3744	⊢ {A, B, C} = ({A, B} ∪ {C})
cuni 3892	class ∪A
df-uni 3893	⊢ ∪A = {x ∣ ∃y(x ∈ y ∧ y ∈ A)}
cint 3927	class ∩A
df-int 3928	⊢ ∩A = {x ∣ ∀y(y ∈ A → x ∈ y)}
ciun 3970	class ∪x ∈ A B
ciin 3971	class ∩x ∈ A B
df-iun 3972	⊢ ∪x ∈ A B = {y ∣ ∃x ∈ A y ∈ B}
df-iin 3973	⊢ ∩x ∈ A B = {y ∣ ∀x ∈ A y ∈ B}
copk 4058	class ⟪A, B⟫
df-opk 4059	⊢ ⟪A, B⟫ = {{A}, {A, B}}
ax-nin 4079	⊢ ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y))
ax-xp 4080	⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(z = ⟪w, t⟫ ∧ t ∈ x))
ax-cnv 4081	⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
ax-1c 4082	⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z))
ax-sset 4083	⊢ ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))
ax-si 4084	⊢ ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
ax-ins2 4085	⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
ax-ins3 4086	⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
ax-typlower 4087	⊢ ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x)
ax-sn 4088	⊢ ∃y∀z(z ∈ y ↔ z = x)
cuni1 4134	class ⋃1A
c1c 4135	class 1c
cpw1 4136	class 𝒫1A
df-1c 4137	⊢ 1c = {x ∣ ∃y x = {y}}
df-pw1 4138	⊢ 𝒫1A = (𝒫 A ∩ 1c)
df-uni1 4139	⊢ ⋃1A = ∪(A ∩ 1c)
cxpk 4175	class (A ×k B)
ccnvk 4176	class ◡kA
cins2k 4177	class Ins2k A
cins3k 4178	class Ins3k A
cp6 4179	class P6 A
cimak 4180	class (A “k B)
ccomk 4181	class (A ∘k B)
csik 4182	class SIk A
cimagek 4183	class ImagekA
cssetk 4184	class Sk
cidk 4185	class Ik
df-xpk 4186	⊢ (A ×k B) = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))}
df-cnvk 4187	⊢ ◡kA = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)}
df-ins2k 4188	⊢ Ins2k A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, v⟫ ∈ A))}
df-ins3k 4189	⊢ Ins3k A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))}
df-imak 4190	⊢ (A “k B) = {x ∣ ∃y ∈ B ⟪y, x⟫ ∈ A}
df-cok 4191	⊢ (A ∘k B) = (( Ins2k A ∩ Ins3k ◡kB) “k V)
df-p6 4192	⊢ P6 A = {x ∣ (V ×k {{x}}) ⊆ A}
df-sik 4193	⊢ SIk A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))}
df-ssetk 4194	⊢ Sk = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y ⊆ z)}
df-imagek 4195	⊢ ImagekA = ((V ×k V) ∖ (( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A)) “k 𝒫1𝒫11c))
df-idk 4196	⊢ Ik = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y = z)}
cio 4338	class (℩xφ)
df-iota 4340	⊢ (℩xφ) = ∪{y ∣ {x ∣ φ} = {y}}
cnnc 4374	class Nn
c0c 4375	class 0c
cplc 4376	class (A +c B)
cfin 4377	class Fin
df-0c 4378	⊢ 0c = {∅}
df-addc 4379	⊢ (A +c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
df-nnc 4380	⊢ Nn = ∩{b ∣ (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)}
df-fin 4381	⊢ Fin = ∪ Nn
clefin 4433	class ≤fin
cltfin 4434	class <fin
cncfin 4435	class Ncfin A
ctfin 4436	class Tfin A
cevenfin 4437	class Evenfin
coddfin 4438	class Oddfin
wsfin 4439	wff Sfin (A, B)
cspfin 4440	class Spfin
df-lefin 4441	⊢ ≤fin = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}
df-ltfin 4442	⊢ <fin = {x ∣ ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))}
df-ncfin 4443	⊢ Ncfin A = (℩x(x ∈ Nn ∧ A ∈ x))
df-tfin 4444	⊢ Tfin M = if(M = ∅, ∅, (℩n(n ∈ Nn ∧ ∃a ∈ M 𝒫1a ∈ n)))
df-evenfin 4445	⊢ Evenfin = {x ∣ (∃n ∈ Nn x = (n +c n) ∧ x ≠ ∅)}
df-oddfin 4446	⊢ Oddfin = {x ∣ (∃n ∈ Nn x = ((n +c n) +c 1c) ∧ x ≠ ∅)}
df-sfin 4447	⊢ ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(𝒫1a ∈ M ∧ 𝒫 a ∈ N)))
df-spfin 4448	⊢ Spfin = ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}
cop 4562	class ⟨A, B⟩
cphi 4563	class Phi A
cproj1 4564	class Proj1 A
cproj2 4565	class Proj2 A
df-phi 4566	⊢ Phi A = {y ∣ ∃x ∈ A y = if(x ∈ Nn , (x +c 1c), x)}
df-op 4567	⊢ ⟨A, B⟩ = ({x ∣ ∃y ∈ A x = Phi y} ∪ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})})
df-proj1 4568	⊢ Proj1 A = {x ∣ Phi x ∈ A}
df-proj2 4569	⊢ Proj2 A = {x ∣ ( Phi x ∪ {0c}) ∈ A}
copab 4623	class {⟨x, y⟩ ∣ φ}
df-opab 4624	⊢ {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}
wbr 4640	wff ARB
df-br 4641	⊢ (ARB ↔ ⟨A, B⟩ ∈ R)
c1st 4718	class 1st
cswap 4719	class Swap
csset 4720	class S
csi 4721	class SI A
ccom 4722	class (A ∘ B)
cima 4723	class (A “ B)
df-1st 4724	⊢ 1st = {⟨x, y⟩ ∣ ∃z x = ⟨y, z⟩}
df-swap 4725	⊢ Swap = {⟨x, y⟩ ∣ ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)}
df-sset 4726	⊢ S = {⟨x, y⟩ ∣ x ⊆ y}
df-co 4727	⊢ (A ∘ B) = {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}
df-ima 4728	⊢ (A “ B) = {x ∣ ∃y ∈ B yAx}
df-si 4729	⊢ SI A = {⟨x, y⟩ ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)}
cep 4763	class E
cid 4764	class I
df-eprel 4765	⊢ E = {⟨x, y⟩ ∣ x ∈ y}
df-id 4768	⊢ I = {⟨x, y⟩ ∣ x = y}
cxp 4771	class (A × B)
ccnv 4772	class ◡A
cdm 4773	class dom A
crn 4774	class ran A
cres 4775	class (A ↾ B)
wfun 4776	wff Fun A
wfn 4777	wff A Fn B
wf 4778	wff F:A–→B
wf1 4779	wff F:A–1-1→B
wfo 4780	wff F:A–onto→B
wf1o 4781	wff F:A–1-1-onto→B
cfv 4782	class (F ‘A)
wiso 4783	wff H Isom R, S (A, B)
c2nd 4784	class 2nd
df-xp 4785	⊢ (A × B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ B)}
df-cnv 4786	⊢ ◡A = {⟨x, y⟩ ∣ yAx}
df-rn 4787	⊢ ran A = (A “ V)
df-dm 4788	⊢ dom A = ran ◡A
df-res 4789	⊢ (A ↾ B) = (A ∩ (B × V))
df-fun 4790	⊢ (Fun A ↔ (A ∘ ◡A) ⊆ I )
df-fn 4791	⊢ (A Fn B ↔ (Fun A ∧ dom A = B))
df-f 4792	⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))
df-f1 4793	⊢ (F:A–1-1→B ↔ (F:A–→B ∧ Fun ◡F))
df-fo 4794	⊢ (F:A–onto→B ↔ (F Fn A ∧ ran F = B))
df-f1o 4795	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))
df-fv 4796	⊢ (F ‘A) = (℩xAFx)
df-iso 4797	⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))
df-2nd 4798	⊢ 2nd = {⟨x, y⟩ ∣ ∃z x = ⟨z, y⟩}
co 5526	class (AFB)
df-ov 5527	⊢ (AFB) = (F ‘⟨A, B⟩)
coprab 5528	class {⟨⟨x, y⟩, z⟩ ∣ φ}
df-oprab 5529	⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
cmpt 5652	class (x ∈ A ↦ B)
df-mpt 5653	⊢ (x ∈ A ↦ B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}
cmpt2 5654	class (x ∈ A, y ∈ B ↦ C)
df-mpt2 5655	⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}
ctxp 5736	class (A ⊗ B)
df-txp 5737	⊢ (A ⊗ B) = ((◡1st ∘ A) ∩ (◡2nd ∘ B))
cpprod 5738	class PProd (A, B)
df-pprod 5739	⊢ PProd (A, B) = ((A ∘ 1st ) ⊗ (B ∘ 2nd ))
cfix 5740	class Fix A
df-fix 5741	⊢ Fix A = ran (A ∩ I )
ccup 5742	class Cup
df-cup 5743	⊢ Cup = (x ∈ V, y ∈ V ↦ (x ∪ y))
cdisj 5744	class Disj
df-disj 5745	⊢ Disj = {⟨x, y⟩ ∣ (x ∩ y) = ∅}
caddcfn 5746	class AddC
df-addcfn 5747	⊢ AddC = (x ∈ V, y ∈ V ↦ (x +c y))
ccompose 5748	class Compose
df-compose 5749	⊢ Compose = (x ∈ V, y ∈ V ↦ (x ∘ y))
cins2 5750	class Ins2 A
df-ins2 5751	⊢ Ins2 A = (V ⊗ A)
cins3 5752	class Ins3 A
df-ins3 5753	⊢ Ins3 A = (A ⊗ V)
cimage 5754	class ImageA
df-image 5755	⊢ ImageA = ∼ (( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A)) “ 1c)
cins4 5756	class Ins4 A
df-ins4 5757	⊢ Ins4 A = (◡(1st ⊗ ((1st ∘ 2nd ) ⊗ ((1st ∘ 2nd ) ∘ 2nd ))) “ A)
csi3 5758	class SI3 A
df-si3 5759	⊢ SI3 A = (( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) “ 𝒫1A)
cfuns 5760	class Funs
df-funs 5761	⊢ Funs = {f ∣ Fun f}
cfns 5762	class Fns
df-fns 5763	⊢ Fns = {⟨f, a⟩ ∣ f Fn a}
ccross 5764	class Cross
df-cross 5765	⊢ Cross = (x ∈ V, y ∈ V ↦ (x × y))
cpw1fn 5766	class Pw1Fn
df-pw1fn 5767	⊢ Pw1Fn = (x ∈ 1c ↦ 𝒫1∪x)
cfullfun 5768	class FullFun F
df-fullfun 5769	⊢ FullFun F = ((( I ∘ F) ∖ ( ∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅}))
cdomfn 5770	class Dom
df-domfn 5771	⊢ Dom = (x ∈ V ↦ dom x)
cranfn 5772	class Ran
df-ranfn 5773	⊢ Ran = (x ∈ V ↦ ran x)
cclos1 5873	class Clos1 (A, R)
df-clos1 5874	⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)}
ctrans 5889	class Trans
cref 5890	class Ref
cantisym 5891	class Antisym
cpartial 5892	class Po
cconnex 5893	class Connex
cstrict 5894	class Or
cfound 5895	class Fr
cwe 5896	class We
cext 5897	class Ext
csym 5898	class Sym
cer 5899	class Er
df-trans 5900	⊢ Trans = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)}
df-ref 5901	⊢ Ref = {⟨r, a⟩ ∣ ∀x ∈ a xrx}
df-antisym 5902	⊢ Antisym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)}
df-partial 5903	⊢ Po = (( Ref ∩ Trans ) ∩ Antisym )
df-connex 5904	⊢ Connex = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)}
df-strict 5905	⊢ Or = ( Po ∩ Connex )
df-found 5906	⊢ Fr = {⟨r, a⟩ ∣ ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))}
df-we 5907	⊢ We = ( Or ∩ Fr )
df-ext 5908	⊢ Ext = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)}
df-sym 5909	⊢ Sym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry → yrx)}
df-er 5910	⊢ Er = ( Sym ∩ Trans )
cec 5946	class [A]R
cqs 5947	class (A / R)
df-ec 5948	⊢ [A]R = (R “ {A})
df-qs 5952	⊢ (A / R) = {y ∣ ∃x ∈ A y = [x]R}
cmap 6000	class ↑m
cpm 6001	class ↑pm
df-map 6002	⊢ ↑m = (x ∈ V, y ∈ V ↦ {f ∣ f:y–→x})
df-pm 6003	⊢ ↑pm = (x ∈ V, y ∈ V ↦ {f ∈ 𝒫 (y × x) ∣ Fun f})
cen 6029	class ≈
df-en 6030	⊢ ≈ = {⟨x, y⟩ ∣ ∃f f:x–1-1-onto→y}
cncs 6089	class NC
clec 6090	class ≤c
cltc 6091	class <c
cnc 6092	class Nc A
cmuc 6093	class ·c
ctc 6094	class Tc A
c2c 6095	class 2c
c3c 6096	class 3c
cce 6097	class ↑c
ctcfn 6098	class TcFn
df-ncs 6099	⊢ NC = (V / ≈ )
df-lec 6100	⊢ ≤c = {⟨a, b⟩ ∣ ∃x ∈ a ∃y ∈ b x ⊆ y}
df-ltc 6101	⊢ <c = ( ≤c ∖ I )
df-nc 6102	⊢ Nc A = [A] ≈
df-muc 6103	⊢ ·c = (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)})
df-tc 6104	⊢ Tc A = (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc 𝒫1x))
df-2c 6105	⊢ 2c = Nc {∅, V}
df-3c 6106	⊢ 3c = Nc {∅, V, (V ∖ {∅})}
df-ce 6107	⊢ ↑c = (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(𝒫1a ∈ n ∧ 𝒫1b ∈ m ∧ g ≈ (a ↑m b))})
df-tcfn 6108	⊢ TcFn = (x ∈ 1c ↦ Tc ∪x)
cspac 6274	class Spac
df-spac 6275	⊢ Spac = (m ∈ NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
cfrec 6310	class FRec (F, I)
df-frec 6311	⊢ FRec (F, I) = Clos1 ({⟨0c, I⟩}, PProd ((x ∈ V ↦ (x +c 1c)), F))
ccan 6324	class Can
df-can 6325	⊢ Can = {x ∣ 𝒫1x ≈ x}
cscan 6326	class SCan
df-scan 6327	⊢ SCan = {x ∣ (y ∈ x ↦ {y}) ∈ V}