Theorem List for New Foundations Explorer - 5801-5900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | imageex 5801 |
The image function of a set is a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ ImageA
∈ V |
|
Theorem | dmtxp 5802 |
The domain of a tail cross product is the intersection of the domains of
its arguments. (Contributed by SF, 18-Feb-2015.)
|
⊢ dom (R
⊗ S) = (dom R ∩ dom S) |
|
Theorem | txpcofun 5803 |
Composition distributes over tail cross product in the case of a
function. (Contributed by SF, 18-Feb-2015.)
|
⊢ Fun F ⇒ ⊢ ((R
⊗ S) ∘ F) =
((R ∘
F) ⊗ (S ∘ F)) |
|
Theorem | fntxp 5804 |
If F and G are functions, then their tail cross
product is a
function over the intersection of their domains. (Contributed by SF,
24-Feb-2015.)
|
⊢ ((F Fn
A ∧
G Fn B) → (F
⊗ G) Fn (A ∩ B)) |
|
Theorem | otsnelsi3 5805 |
Ordered triple membership in triple singleton image. (Contributed by
SF, 12-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V ⇒ ⊢ (〈{A}, 〈{B}, {C}〉〉 ∈ SI3 R ↔ 〈A, 〈B, C〉〉 ∈ R) |
|
Theorem | si3ex 5806 |
SI3 preserves
sethood. (Contributed by SF, 12-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ SI3 A ∈
V |
|
Theorem | releqel 5807* |
Lemma to turn a membership condition into an equality condition.
(Contributed by SF, 9-Mar-2015.)
|
⊢ T ∈ V
& ⊢ (〈{y}, T〉 ∈ R ↔ y
∈ A) ⇒ ⊢ (〈x, T〉 ∈ ∼ ((
Ins3 S ⊕
Ins2 R)
“ 1c) ↔ x =
A) |
|
Theorem | releqmpt 5808* |
Equality condition for a mapping. (Contributed by SF, 9-Mar-2015.)
|
⊢ (〈{y}, x〉 ∈ R ↔ y
∈ V) ⇒ ⊢ ((A ×
V) ∩ ◡ ∼ (( Ins3 S ⊕ Ins2 R) “
1c)) = (x ∈ A ↦ V) |
|
Theorem | releqmpt2 5809* |
Equality condition for a mapping operation. (Contributed by SF,
13-Feb-2015.)
|
⊢ (〈{z}, 〈x, y〉〉 ∈ R ↔
z ∈
V) ⇒ ⊢ (((A
× B) × V) ∖ (( Ins2 S ⊕ Ins3 R) “ 1c)) = (x ∈ A, y ∈ B ↦ V) |
|
Theorem | mptexlem 5810 |
Lemma for the existence of a mapping. (Contributed by SF,
9-Mar-2015.)
|
⊢ A ∈ V
& ⊢ R ∈ V ⇒ ⊢ ((A ×
V) ∩ ◡ ∼ (( Ins3 S ⊕ Ins2 R) “
1c)) ∈ V |
|
Theorem | mpt2exlem 5811 |
Lemma for the existence of a double mapping. (Contributed by SF,
13-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ R ∈ V ⇒ ⊢ (((A
× B) × V) ∖ (( Ins2 S ⊕ Ins3 R) “ 1c)) ∈ V |
|
Theorem | cupvalg 5812 |
The value of the little cup function. (Contributed by SF,
11-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(A Cup
B) = (A ∪ B)) |
|
Theorem | fncup 5813 |
The cup function is a function over the universe. (Contributed by SF,
11-Feb-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
|
⊢ Cup Fn
V |
|
Theorem | brcupg 5814 |
Binary relationship form of the cup function. (Contributed by SF,
11-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(〈A,
B〉 Cup C ↔
C = (A
∪ B))) |
|
Theorem | brcup 5815 |
Binary relationship form of the cup function. (Contributed by SF,
11-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉 Cup C ↔ C =
(A ∪ B)) |
|
Theorem | cupex 5816 |
The little cup function is a set. (Contributed by SF, 11-Feb-2015.)
|
⊢ Cup ∈ V |
|
Theorem | composevalg 5817 |
The value of the composition function. (Contributed by Scott Fenton,
19-Apr-2021.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(A Compose
B) = (A ∘ B)) |
|
Theorem | composefn 5818 |
The compose function is a function over the universe. (Contributed by
Scott Fenton, 19-Apr-2021.)
|
⊢ Compose Fn
V |
|
Theorem | brcomposeg 5819 |
Binary relationship form of the compose function. (Contributed by Scott
Fenton, 19-Apr-2021.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(〈A,
B〉 Compose C ↔
(A ∘
B) = C)) |
|
Theorem | composeex 5820 |
The compose function is a set. (Contributed by Scott Fenton,
19-Apr-2021.)
|
⊢ Compose ∈ V |
|
Theorem | brdisjg 5821 |
The binary relationship form of the Disj relationship. (Contributed
by SF, 11-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(A Disj
B ↔ (A ∩ B) =
∅)) |
|
Theorem | brdisj 5822 |
The binary relationship form of the Disj relationship. (Contributed
by SF, 11-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A Disj B ↔
(A ∩ B) = ∅) |
|
Theorem | disjex 5823 |
The disjointedness relationship is a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ Disj ∈ V |
|
Theorem | addcfnex 5824 |
The cardinal addition function exists. (Contributed by SF,
12-Feb-2015.)
|
⊢ AddC ∈ V |
|
Theorem | addcfn 5825 |
AddC is a function over the
universe. (Contributed by SF,
2-Mar-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
|
⊢ AddC Fn
V |
|
Theorem | braddcfn 5826 |
Binary relationship form of the AddC
function. (Contributed by SF,
2-Mar-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉 AddC C ↔ (A
+c B) = C) |
|
Theorem | epprc 5827 |
The membership relationship is a proper class. This theorem together with
vvex 4109 demonstrates the basic idea behind New
Foundations: since
x ∈ y is
not a stratified relationship, then it does not have a
realization as a set of ordered pairs, but since x = x is
stratified,
then it does have a realization as a set. (Contributed by SF,
20-Feb-2015.)
|
⊢ ¬ E ∈
V |
|
Theorem | funsex 5828 |
The class of all functions forms a set. (Contributed by SF,
18-Feb-2015.)
|
⊢ Funs ∈ V |
|
Theorem | elfuns 5829 |
Membership in the set of all functions. (Contributed by SF,
23-Feb-2015.)
|
⊢ F ∈ V ⇒ ⊢ (F ∈ Funs ↔ Fun
F) |
|
Theorem | elfunsg 5830 |
Membership in the set of all functions. (Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (F ∈ V →
(F ∈
Funs ↔ Fun F)) |
|
Theorem | elfunsi 5831 |
Membership in the set of all functions implies functionhood. (Contributed
by Scott Fenton, 31-Jul-2019.)
|
⊢ (F ∈ Funs → Fun
F) |
|
Theorem | fnsex 5832 |
The function with domain relationship exists. (Contributed by SF,
23-Feb-2015.)
|
⊢ Fns ∈ V |
|
Theorem | brfns 5833 |
Binary relationship form of Fns
relationship. (Contributed by SF,
23-Feb-2015.)
|
⊢ F ∈ V ⇒ ⊢ (F Fns A ↔
F Fn A) |
|
Theorem | pprodeq1 5834 |
Equality theorem for parallel product. (Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (A =
B → PProd (A, C) = PProd (B, C)) |
|
Theorem | pprodeq2 5835 |
Equality theorem for parallel product. (Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (A =
B → PProd (C, A) = PProd (C, B)) |
|
Theorem | qrpprod 5836 |
A quadratic relationship over a parallel product. (Contributed by SF,
24-Feb-2015.)
|
⊢ (〈A, B〉 PProd (R, S)〈C, D〉 ↔
(ARC ∧ BSD)) |
|
Theorem | pprodexg 5837 |
The parallel product of two sets is a set. (Contributed by SF,
24-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
PProd (A,
B) ∈
V) |
|
Theorem | pprodex 5838 |
The parallel product of two sets is a set. (Contributed by SF,
24-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ PProd (A, B) ∈ V |
|
Theorem | brpprod 5839* |
Binary relationship over a parallel product. (Contributed by SF,
24-Feb-2015.)
|
⊢ (A PProd (R, S)B ↔
∃x∃y∃z∃w(A = 〈x, y〉 ∧ B = 〈z, w〉 ∧ (xRz ∧ ySw))) |
|
Theorem | dmpprod 5840 |
The domain of a parallel product. (Contributed by SF, 24-Feb-2015.)
|
⊢ dom PProd
(A, B)
= (dom A × dom B) |
|
Theorem | cnvpprod 5841 |
The converse of a parallel product. (Contributed by SF, 24-Feb-2015.)
|
⊢ ◡ PProd (A, B) = PProd (◡A,
◡B) |
|
Theorem | rnpprod 5842 |
The range of a parallel product. (Contributed by SF, 24-Feb-2015.)
|
⊢ ran PProd
(A, B)
= (ran A × ran B) |
|
Theorem | fnpprod 5843 |
Functionhood law for parallel product. (Contributed by SF,
24-Feb-2015.)
|
⊢ ((F Fn
A ∧
G Fn B) → PProd
(F, G)
Fn (A × B)) |
|
Theorem | f1opprod 5844 |
The parallel product of two bijections is a bijection. (Contributed by
SF, 24-Feb-2015.)
|
⊢ ((F:A–1-1-onto→C ∧ G:B–1-1-onto→D) →
PProd (F,
G):(A
× B)–1-1-onto→(C
× D)) |
|
Theorem | ovcross 5845 |
The value of the cross product function. (Contributed by SF,
24-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(A Cross
B) = (A × B)) |
|
Theorem | fncross 5846 |
The cross product function is a function over (V × V)
(Contributed by SF, 24-Feb-2015.)
|
⊢ Cross Fn
V |
|
Theorem | dmcross 5847 |
The domain of the cross product function. (Contributed by SF,
24-Feb-2015.)
|
⊢ dom Cross =
V |
|
Theorem | brcrossg 5848 |
Binary relationship over the cross product function. (Contributed by SF,
24-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(〈A,
B〉 Cross C ↔
C = (A
× B))) |
|
Theorem | brcross 5849 |
Binary relationship over the cross product function. (Contributed by
SF, 24-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉 Cross C ↔ C =
(A × B)) |
|
Theorem | crossex 5850 |
The function mapping x and
y to their cross product is a
set.
(Contributed by SF, 11-Feb-2015.)
|
⊢ Cross ∈ V |
|
Theorem | pw1fnval 5851 |
The value of the unit power class function. (Contributed by SF,
25-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ ( Pw1Fn
‘{A}) = ℘1A |
|
Theorem | pw1fnex 5852 |
The unit power class function is a set. (Contributed by SF,
25-Feb-2015.)
|
⊢ Pw1Fn ∈ V |
|
Theorem | fnpw1fn 5853 |
Functionhood statement for Pw1Fn.
(Contributed by SF,
25-Feb-2015.)
|
⊢ Pw1Fn Fn
1c |
|
Theorem | brpw1fn 5854 |
Binary relationship form of Pw1Fn.
(Contributed by SF,
25-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ ({A} Pw1Fn B ↔
B = ℘1A) |
|
Theorem | pw1fnf1o 5855 |
Pw1Fn is a one-to-one function with
domain 1c and range
℘1c.
(Contributed by SF, 26-Feb-2015.)
|
⊢ Pw1Fn
:1c–1-1-onto→℘1c |
|
Theorem | fnfullfunlem1 5856* |
Lemma for fnfullfun 5858. Binary relationship over part one of the
full
function definition. (Contributed by SF, 9-Mar-2015.)
|
⊢ (A(( I
∘ F)
∖ ( ∼ I ∘ F))B ↔ (AFB ∧ ∀x(AFx → x =
B))) |
|
Theorem | fnfullfunlem2 5857 |
Lemma for fnfullfun 5858. Part one of the full function operator
yields a
function. (Contributed by SF, 9-Mar-2015.)
|
⊢ Fun (( I ∘
F) ∖ (
∼ I ∘ F)) |
|
Theorem | fnfullfun 5858 |
The full function operator yields a function over V.
(Contributed
by SF, 9-Mar-2015.)
|
⊢ FullFun F Fn V |
|
Theorem | fullfunexg 5859 |
The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
|
⊢ (F ∈ V →
FullFun F
∈ V) |
|
Theorem | fullfunex 5860 |
The full function of a set is a set. (Contributed by SF,
9-Mar-2015.)
|
⊢ F ∈ V ⇒ ⊢ FullFun F ∈
V |
|
Theorem | fvfullfunlem1 5861* |
Lemma for fvfullfun 5864. Calculate the domain of part one of the
full
function definition. (Contributed by SF, 9-Mar-2015.)
|
⊢ dom (( I ∘
F) ∖ (
∼ I ∘ F)) = {x ∣ ∃!y xFy} |
|
Theorem | fvfullfunlem2 5862 |
Lemma for fvfullfun 5864. Part one of the full function definition is
a
subset of the function. (Contributed by SF, 9-Mar-2015.)
|
⊢ (( I ∘
F) ∖ (
∼ I ∘ F)) ⊆ F |
|
Theorem | fvfullfunlem3 5863 |
Lemma for fvfullfun 5864. Part one of the full function definition
agrees
with the set itself over its domain. (Contributed by SF,
9-Mar-2015.)
|
⊢ (A ∈ dom (( I ∘
F) ∖ (
∼ I ∘ F)) → ((( I ∘ F) ∖ ( ∼ I ∘
F)) ‘A) = (F
‘A)) |
|
Theorem | fvfullfun 5864 |
The value of the full function definition agrees with the function value
everywhere. (Contributed by SF, 9-Mar-2015.)
|
⊢ ( FullFun F ‘A) =
(F ‘A) |
|
Theorem | brfullfung 5865 |
Binary relationship of the full function operation. (Contributed by SF,
9-Mar-2015.)
|
⊢ (A ∈ V →
(A FullFun
FB
↔ (F ‘A) = B)) |
|
Theorem | brfullfun 5866 |
Binary relationship of the full function operation. (Contributed by SF,
9-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ (A FullFun FB ↔ (F
‘A) = B) |
|
Theorem | brfullfunop 5867 |
Binary relationship of the full function operation over an ordered pair.
(Contributed by SF, 9-Mar-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉 FullFun FC ↔
(AFB) = C) |
|
Theorem | fvdomfn 5868 |
Calculate the value of the domain function. (Contributed by Scott
Fenton, 9-Aug-2019.)
|
⊢ (A ∈ V → (
Dom ‘A)
= dom A) |
|
Theorem | fvranfn 5869 |
Calculate the value of the range function. (Contributed by Scott
Fenton, 9-Aug-2019.)
|
⊢ (A ∈ V → (
Ran ‘A)
= ran A) |
|
Theorem | domfnex 5870 |
The domain function is stratified. (Contributed by Scott Fenton,
9-Aug-2019.)
|
⊢ Dom ∈ V |
|
Theorem | ranfnex 5871 |
The range function is stratified. (Contributed by Scott Fenton,
9-Aug-2019.)
|
⊢ Ran ∈ V |
|
2.3.11 Closure operation
|
|
Syntax | cclos1 5872 |
Extend the definition of a class to include the closure operation.
|
class
Clos1 (A, R) |
|
Definition | df-clos1 5873* |
Define the closure operation. A modified version of the definition from
[Rosser] p. 245. (Contributed by SF,
11-Feb-2015.)
|
⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “
a) ⊆
a)} |
|
Theorem | clos1eq1 5874 |
Equality law for closure. (Contributed by SF, 11-Feb-2015.)
|
⊢ (S =
T → Clos1
(S, R) = Clos1 (T, R)) |
|
Theorem | clos1eq2 5875 |
Equality law for closure. (Contributed by SF, 11-Feb-2015.)
|
⊢ (R =
T → Clos1
(S, R) = Clos1 (S, T)) |
|
Theorem | clos1ex 5876 |
The closure of a set under a set is a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ S ∈ V
& ⊢ R ∈ V ⇒ ⊢ Clos1 (S, R) ∈ V |
|
Theorem | clos1exg 5877 |
The closure of a set under a set is a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ ((S ∈ V ∧ R ∈ W) →
Clos1 (S,
R) ∈
V) |
|
Theorem | clos1base 5878 |
The initial set of a closure is a subset of the closure. Theorem
IX.5.13 of [Rosser] p. 246. (Contributed
by SF, 13-Feb-2015.)
|
⊢ C = Clos1 (S, R) ⇒ ⊢ S ⊆ C |
|
Theorem | clos1conn 5879 |
If a class is connected to an element of a closure via R, then it
is a member of the closure. Theorem IX.5.14 of [Rosser] p. 246.
(Contributed by SF, 13-Feb-2015.)
|
⊢ C = Clos1 (S, R) ⇒ ⊢ ((A ∈ C ∧ ARB) →
B ∈
C) |
|
Theorem | clos1induct 5880* |
Inductive law for closure. If the base set is a subset of X, and
X is closed under
R, then the closure is a
subset of X.
Theorem IX.5.15 of [Rosser] p. 247.
(Contributed by SF,
11-Feb-2015.)
|
⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ ((X ∈ V ∧ S ⊆ X ∧ ∀x ∈ C ∀z((x ∈ X ∧ xRz) →
z ∈
X)) → C ⊆ X) |
|
Theorem | clos1is 5881* |
Induction scheme for closures. Hypotheses one through three set up
existence properties, hypothesis four sets up stratification, hypotheses
five through seven set up implicit substitution, and hypotheses eight
and nine set up the base and induction steps. (Contributed by SF,
13-Feb-2015.)
|
⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R)
& ⊢ {x ∣ φ}
∈ V
& ⊢ (x =
y → (φ ↔ ψ))
& ⊢ (x =
z → (φ ↔ χ))
& ⊢ (x =
A → (φ ↔ θ))
& ⊢ (x ∈ S →
φ)
& ⊢ ((y ∈ C ∧ yRz ∧ ψ) →
χ) ⇒ ⊢ (A ∈ C →
θ) |
|
Theorem | clos1basesuc 5882* |
A member of a closure is either in the base set or connected to another
member by R. Theorem
IX.5.16 of [Rosser] p. 248. (Contributed by
SF, 13-Feb-2015.)
|
⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ (A ∈ C ↔
(A ∈
S ∨ ∃x ∈ C xRA)) |
|
Theorem | clos1baseima 5883 |
A closure is equal to the base set together with the image of the
closure under R.
Theorem X.4.37 of [Rosser] p. 303. (Contributed
by SF, 10-Mar-2015.)
|
⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ C =
(S ∪ (R “ C)) |
|
Theorem | clos1basesucg 5884* |
A member of a closure is either in the base set or connected to another
member by R. Theorem
IX.5.16 of [Rosser] p. 248. (Contributed by
Scott Fenton, 31-Jul-2019.)
|
⊢ C = Clos1 (S, R) ⇒ ⊢ ((S ∈ V ∧ R ∈ W) →
(A ∈
C ↔ (A ∈ S ∨ ∃x ∈ C xRA))) |
|
Theorem | dfnnc3 5885 |
The finite cardinals as expressed via the closure operation. Theorem
X.1.3 of [Rosser] p. 276. (Contributed
by SF, 12-Feb-2015.)
|
⊢ Nn = Clos1 ({0c}, (x ∈ V ↦ (x
+c 1c))) |
|
Theorem | clos1nrel 5886 |
The value of a closure when the base set is not related to anything in
R. (Contributed by
SF, 13-Mar-2015.)
|
⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ ((R “
S) = ∅
→ C = S) |
|
Theorem | clos10 5887 |
The value of a closure over an empty base set. (Contributed by Scott
Fenton, 31-Jul-2019.)
|
⊢ R ∈ V
& ⊢ C = Clos1 (∅, R) ⇒ ⊢ C = ∅ |
|
2.4 Orderings
|
|
2.4.1 Basic ordering relationships
|
|
Syntax | ctrans 5888 |
Extend the definition of a class to include the set of all transitive
relationships.
|
class
Trans |
|
Syntax | cref 5889 |
Extend the definition of a class to include the set of all reflexive
relationships.
|
class
Ref |
|
Syntax | cantisym 5890 |
Extend the definition of a class to include the set of all antisymmetric
relationships.
|
class
Antisym |
|
Syntax | cpartial 5891 |
Extend the definition of a class to include the set of all partial
orderings.
|
class
Po |
|
Syntax | cconnex 5892 |
Extend the definition of a class to include the set of all connected
relationships.
|
class
Connex |
|
Syntax | cstrict 5893 |
Extend the definition of a class to include the set of all strict linear
orderings.
|
class
Or |
|
Syntax | cfound 5894 |
Extend the definition of a class to include the set of all founded
relationships.
|
class
Fr |
|
Syntax | cwe 5895 |
Extend the definition of a class to include the set of all well-ordered
relationships.
|
class
We |
|
Syntax | cext 5896 |
Extend the definition of a class to include the set of all extensional
relationships.
|
class
Ext |
|
Syntax | csym 5897 |
Extend the definition of a class to include the symmetric
relationships.
|
class
Sym |
|
Syntax | cer 5898 |
Extend the definition of a class to include the equivalence
relationships.
|
class
Er |
|
Definition | df-trans 5899* |
Define the set of all transitive relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
⊢ Trans = {〈r, a〉 ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) →
xrz)} |
|
Definition | df-ref 5900* |
Define the set of all reflexive relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
⊢ Ref = {〈r, a〉 ∣ ∀x ∈ a xrx} |