Spring 2002 - Math 235A - Exercise 1
Exercise 1 asks us to prove that given two sets A and B that there is a
set of all functions from B to A.
Informal Proof
The main lemma that this theorem rests on is that for any relation R
whose domain is a subset of some B and whose range is a subset of some
A, then R is an element of the power set of (B × A). This is
‘obvious’ from the definition of relation, and I will not
prove it here.
Let
BA = {f ∈ ℘(B × A) | f is a function ∧ (dom f)=B ∧ (rng f) ⊆ A}.
By the definition of BA it is clear that every element is a function
from B to A.
Let f be a function from B to A. By definition f is also a relation.
Since f is a function from B, (dom f)=B, and hence (dom f) ⊆ B.
Since f is a function to A, (rng f) ⊆ A.
By the above lemma, f is in ℘(B × A).
Now since f is a function from A to B, then f ∈ BA.
So BA is the required set.
Although the above argument might be persuasive, is it really
correct? Is the ‘obvious’ lemma give above true? Should I
have added more details? Are you, the reader, still skeptical? To
really prove the theorem true beyond a reasonable doubt, we should appeal
to a complete formal proof that has been machine verified.
Formal Proof
Below is the formal proof of the assigned question. Of course this
proof relies on some existing definitions and theorems. The statements
of these definitions and theorems are also given. Some definitions
have been omitted because they are considered obvious to any reader
familiar with set theory. The entire proof
is given at the end.
I should note that this proof has not been carried out in first
order logic. It has been carried out in higher-order type theory. It is
not clear to me that all the provable formulas that are equivalent to
a first-order formula will be the same as the provable formulas in
first-order logic. Nothing particularly fancy has been used in the proof
here, so the proof should translate with no problems.
Reading the Proof
The proof is given is written in the standard λ-calculus
notation for natural deduction proofs. There is some other notation that
may be less familiar that I will explain.
Ens (short for ensemble) is the type I declared for the universe of
sets. Types such as Ens → Prop can be interpreted as logical
relational symbols. They take sets and return propositions. Types such
as Ens → Ens can be interpreted as logical function symbols.
[A:=expr] defines shorthand. Occurrences of A are
substituted with expr.
Cases A of (exT_intro x _) => x end appears in
many places. Although Cases is a fairly general construction, in this
instance the expression returns a element from an existential proof A
(this is why exT_intro is mentioned). Informally, if we
proved (∃ x∈N)(x is Prime), then saying, “Let y be
such a number” would be valid reasoning.
<type>expr also appears.
This is is similar to a type cast. If type=T1,
expr has type T2, and T1 and T2 are intensionally
equal, then the resulting expression has type T1. Since intensional
equality is decidable, no further annotations are needed.
Definitions
related = λa,R,b:Ens.(<a,b> ∈ R)
: Ens→Ens→Ens→Prop
isRelation =
λR:Ens.
(∀x:Ens)(x ∈ R)→(∃a:Ens)((∃b:Ens)(x=<a,b>))
: Ens→Prop
isFunction =
λf:Ens.
(isRelation f)∧((∀x,y,z:Ens)(related x f y)∧(related x f z)→y=z)
: Ens→Prop
functions =
λa,b:Ens.
[A:=(power (b × a))]
[B:=(Separation A
λx:Ens.(isFunction x)∧(domain x)=b∧((range x) ⊆ a))]
Cases B of (exT_intro x _) ⇒ x end
: Ens→Ens→Ens
Axioms and Lemmas
PI1
: (∀S:Prop; P:(S→Prop))(∃x:S)((P x))→S
PI2
: (∀S:Prop; P:(S→Prop); a:(∃x:S)((P x)))(P (PI1 S P a))
exT_intro
: (∀A:Type; P:(A→Prop); x:A)(P x)→(∃x:A)(P x)
and_ind
: (∀A,B,P:Prop)(A→B→P)→A∧B→P
π1
: (∀A,B:Prop)A∧B→A
π2
: (∀A,B:Prop)A∧B→B
Separation
: (∀a:Ens; P:(Ens→Prop))
(∃x:Ens)((∀y:Ens)(y ∈ x)↔(y ∈ a)∧(P y))
sube1
: (∀a,b:Ens)a=b→(a ⊆ b)
relations1
: (∀a,b,R:Ens)
(isRelation R)∧((domain R) ⊆ b)∧((range R) ⊆ a)
→(R ∈ (power (b × a)))
Proof
The following is a proof of exercise 1,
(∀ a,b,f:Ens)
(f ∈ (functions a b))
↔(isFunction f)∧(domain f)=b∧((range f)
⊆ a).
λa,b,f:Ens.
[A:=(power (b × a))]
[B:=(Separation A
λx:Ens.(isFunction x)∧(domain x)=b∧((range x) ⊆ a))]
[p:=(PI2 Ens
λx:Ens.
(∀ y:Ens)
(y ∈ x)
↔(y ∈ A)
∧(isFunction y)∧(domain y)=b∧((range y) ⊆ a) B)]
<((f ∈ Cases B of (exT_intro x _) ⇒ x end)
→(isFunction f)∧(domain f)=b∧((range f) ⊆ a)),
((isFunction f)∧(domain f)=b∧((range f) ⊆ a)
→(f ∈ Cases B of (exT_intro x _) ⇒ x end))>
{(λH:(f ∈ Cases B of (exT_intro x _) ⇒ x end).
[p1:=(π1
(f ∈ Cases B of (exT_intro x _) ⇒ x end)
→(f ∈ A)
∧(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
(f ∈ A)
∧(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
→(f ∈ Cases B of (exT_intro x _) ⇒ x end) (p f) H)]
(and_ind (f ∈ A)
(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
λ_:(f ∈ A);
H1:((isFunction f)∧(domain f)=b∧((range f) ⊆ a)).
(and_ind (isFunction f) (domain f)=b∧((range f) ⊆ a)
(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
λH2:(isFunction f);
H3:((domain f)=b∧((range f) ⊆ a)).
(and_ind (domain f)=b ((range f) ⊆ a)
(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
λH4:((domain f)=b); H5:((range f) ⊆ a).
<(isFunction f),((domain f)=b∧((range f) ⊆ a))>
{H2,(<((domain f)=b),((range f) ⊆ a)>{H4,H5})}
H3) H1) p1)),
(λH:((isFunction f)∧(domain f)=b∧((range f) ⊆ a)).
(π2
(f ∈ Cases B of (exT_intro x _) ⇒ x end)
→(f ∈ A)∧(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
(f ∈ A)∧(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
→(f ∈ Cases B of (exT_intro x _) ⇒ x end) (p f)
<(f ∈ A),
((isFunction f)∧(domain f)=b∧((range f) ⊆ a))>
{(relations1 a b f
<(isRelation f),
(((domain f) ⊆ b)∧((range f) ⊆ a))>
{(and_ind
(isRelation f)
∧((∀ x,y,z:Ens)(related x f y)∧(related x f z)→y=z)
(domain f)=b∧((range f) ⊆ a) (isRelation f)
λH0:
((isRelation f)
∧((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z));
H1:((domain f)=b∧((range f) ⊆ a)).
(and_ind (isRelation f)
(∀ x,y,z:Ens)(related x f y)∧(related x f z)→y=z
(isRelation f)
λH2:(isRelation f);
_:((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z).
(and_ind (domain f)=b ((range f) ⊆ a)
(isRelation f)
λ_:((domain f)=b); _:((range f) ⊆ a).H2 H1)
H0) H),
(<((domain f) ⊆ b),((range f) ⊆ a)>
{(sube1 (domain f) b
(and_ind
(isRelation f)
∧((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z)
(domain f)=b∧((range f) ⊆ a) (domain f)=b
λH0:
((isRelation f)
∧((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z));
H1:((domain f)=b∧((range f) ⊆ a)).
(and_ind (isRelation f)
(∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z
(domain f)=b
λ_:(isRelation f);
_:((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z).
(and_ind (domain f)=b ((range f) ⊆ a)
(domain f)=b
λH4:((domain f)=b); _:((range f) ⊆ a).
H4 H1) H0) H)),
(and_ind
(isRelation f)
∧((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z)
(domain f)=b∧((range f) ⊆ a)
((range f) ⊆ a)
λH0:
((isRelation f)
∧((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z));
H1:((domain f)=b∧((range f) ⊆ a)).
(and_ind (isRelation f)
(∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z
((range f) ⊆ a)
λ_:(isRelation f);
_:((∀ x,y,z:Ens)
(related x f y)∧(related x f z)→y=z).
(and_ind (domain f)=b ((range f) ⊆ a)
((range f) ⊆ a)
λ_:((domain f)=b); H5:((range f) ⊆ a).H5
H1) H0) H)})}),H}))}
: (∀ a,b,f:Ens)
(f ∈ (functions a b))
↔(isFunction f)∧(domain f)=b∧((range f) ⊆ a)
Complete Proof
The following is the source to the Coq
module that prove this theorem. It does not state the above proof itself,
but lists a series of tactics. These tactics are used by Coq to generate
its proofs. You will note the list of tactics used to generate the last
theorem is much shorter than the proof written out above.
The list of axioms of ZFC is incomplete. Not all the axioms are
needed to do this problem. The other axioms have been omitted because
I am lazy.
This module is available on the web at http://www.math.berkeley.edu/˜roconnor/math235A/zfc1.v. You may
download it and verify the proof yourself.
Proof
Read Module Classical_Type.
Lemma iff_trans : (A,B,C:Prop)(A<->B)->(B<->C)->(A<->C).
Proof.
Tauto.
Qed.
Definition PI1 : (S:Prop)(P:S->Prop)(EXT x:S | (P x))->S :=
[S:Prop][P:S->Prop][a:(EXT x:S | (P x))]
Cases a of (exT_intro x _) => x end.
Definition PI2 : (S:Prop; P:(S->Prop); a:(EXT x:S | (P x)))(P (PI1 S P a)) :=
[S:Prop][P:S->Prop][a:(EXT x:S | (P x))]
<[a:?](P (PI1 S P a))>Cases a of (exT_intro _ x) => x end.
Theorem CHOICE : (S,S':Prop)(P:S->S'->Prop)((x:S)(EXT y:S' | (P x y)))->
(EXT f:S->S' | (z:S)(P z (f z))).
Proof.
Intros S S' P g.
Exists [x:S](PI1 ? ? (g x)).
Intro.
Apply (PI2 ? ? (g z)).
Qed.
Theorem CHOICE2 : (A,B,C:Prop)(P:A->B->C->Prop)
((a:A)(b:B)(EXT c:C | (P a b c))) ->
(EXT f:A->B->C | (a':A)(b':B)(P a' b' (f a' b'))).
Proof.
Intros A B C P g.
Exists [x:A][y:B](PI1 ? ? (g x y)).
Intros.
Apply (PI2 ? ? (g a' b')).
Qed.
Parameter Ens : Prop.
Parameter IN : Ens -> Ens -> Prop.
Definition notIn : Ens -> Ens -> Prop :=
[x:Ens][y:Ens]~(IN x y).
Definition sube : Ens -> Ens -> Prop :=
[x:Ens][y:Ens](z:Ens)((IN z x)->(IN z y)).
Axiom EmptySet : (EXT x:Ens | (y:Ens)~(IN y x)).
Definition emptySet : Ens := (PI1 ? [x:Ens](y:Ens)~(IN y x) EmptySet).
Axiom Extensionality : (a,b,x:Ens)((IN x a)<->(IN x b))->(a==b).
Axiom Pairing : (a,b:Ens)(EXT x:Ens | (y:Ens)(IN y x)<->(y==a \/ y==b)).
Axiom Sum : (a:Ens)(EXT c:Ens | (x:Ens)(IN x c)<->
(EXT y:Ens | (IN y a)/\(IN x y))).
Axiom PowerSet : (a:Ens)(EXT b:Ens | (x:Ens)(IN x b)<->(sube x a)).
Axiom Regularity : (a:Ens)(~(a==emptySet))->(EXT x:Ens | (IN x a)/\
(y:Ens)(IN y x)->(notIn y a)).
Axiom Separation : (a:Ens)(P:Ens->Prop)(EXT x:Ens | (y:Ens)(IN y x)<->
((IN y a)/\(P y))).
Theorem sube1 : (a,b:Ens)(a==b)->(sube a b).
Proof.
Intros.
Rewrite H.
Unfold sube.
Auto.
Qed.
Definition pair : Ens -> Ens -> Ens :=
Cases (CHOICE2 ? ? ? [a,b,x:Ens](y:Ens)(IN y x)<->(y==a \/ y==b) Pairing) of
(exT_intro x _) => x end.
Lemma pair1 : (a,b,c:Ens)(IN c (pair a b))<->(c==a \/ c==b).
Proof.
Intros.
LetTac p := (CHOICE2 ? ? ? [a,b,x:Ens](y:Ens)(IN y x)<->(y==a \/ y==b) Pairing).
LetTac p0 := (PI2 ? [f:Ens->Ens->Ens](a',b',y:Ens)(IN y (f a' b'))<->y==a'\/y==b' p).
Apply p0.
Qed.
Lemma pair2 : (a,b:Ens)(IN a (pair a b)).
Proof.
Intros.
LetTac p := (proj2 ? ? (pair1 a b a)).
Apply p.
Auto.
Qed.
Lemma pair3 : (a,b:Ens)(IN b (pair a b)).
Intros.
LetTac p := (proj2 ? ? (pair1 a b b)).
Apply p.
Auto.
Qed.
Definition single : Ens -> Ens := [a:Ens](pair a a).
Lemma single1 : (a,b:Ens)(IN b (single a))<->(b==a).
Proof.
Intros.
Unfold single.
LetTac p := (pair1 a a b).
Tauto.
Qed.
Lemma single2: (a:Ens)(IN a (single a)).
Proof.
Intro.
Unfold single.
Apply pair2.
Qed.
Definition sum : Ens -> Ens :=
Cases (CHOICE ? ? [a:Ens][c:Ens](x:Ens)(IN x c)<->(EXT y:Ens | (IN y a)/\(IN x y)) Sum) of
(exT_intro x _) => x end.
Lemma sum1 : (a,b:Ens)(IN a (sum b))<->(EXT c:Ens | (IN c b)/\ (IN a c)).
Proof.
LetTac p := (CHOICE ? ? [a:Ens][c:Ens](x:Ens)(IN x c)<->(EXT y:Ens | (IN y a)/\(IN x y)) Sum).
LetTac p0 := (PI2 Ens->Ens [f:Ens->Ens](z,x:Ens)(IN x (f z))<->(EXT y:Ens | (IN y z)/\(IN x y)) p).
Intros.
Apply p0.
Qed.
Definition union : Ens -> Ens -> Ens :=
[a:Ens][b:Ens](sum (pair a b)).
Lemma union1 : (a,b,c:Ens)(EXT y:Ens | (IN y (pair a b))/\(IN c y))<->
((IN c a)\/(IN c b)).
Proof.
Intros.
Constructor.
Intro.
Elim H.
Intros.
Induction H0.
Case ((proj1 ? ? (pair1 a b x)) H0).
Intro.
Rewrite H2 in H1.
Auto.
Intros.
Rewrite H2 in H1.
Auto.
Intro.
Case H.
Intro.
Exists a.
Constructor.
Apply pair2.
Auto.
Intro.
Exists b.
Constructor.
Apply pair3.
Auto.
Qed.
Lemma union2 : (a,b,c:Ens)(IN c (union a b))<->((IN c a)\/(IN c b)).
Proof.
Intros.
Unfold union.
Unfold sum.
LetTac p := (CHOICE Ens Ens
[a0,c0:Ens]
(x:Ens)(IN x c0)<->(EXT y:Ens | (IN y a0)/\(IN x y)) Sum).
LetTac p0 := (PI2 ? [f:Ens->Ens](z,x:Ens)(IN x (f z))<->(EXT y:Ens | (IN y z)/\(IN x y)) p).
Unfold PI1 in p0.
LetTac p1 := (p0 c).
LetTac p2 := (union1 a b c).
Apply iff_trans with (EXT y:Ens | (IN y (pair a b))/\(IN c y)).
Auto.
Auto.
Qed.
Definition power : Ens -> Ens :=
Cases (CHOICE ? ? [a:Ens][b:Ens](x:Ens)(IN x b)<->(sube x a) PowerSet) of
(exT_intro x _) => x end.
Lemma power1 : (a,b:Ens)(IN a (power b))<->(sube a b).
Proof.
LetTac p := (CHOICE ? ? [a:Ens][b:Ens](x:Ens)(IN x b)<->(sube x a) PowerSet).
LetTac p0 := (PI2 Ens->Ens [f:Ens->Ens](z,x:Ens)(IN x (f z))<->(sube x z) p).
Intros.
Apply p0.
Qed.
Definition orderedPair : Ens -> Ens -> Ens :=
[a:Ens][b:Ens](pair (single a) (pair a b)).
Definition crossProd :=
[a:Ens][b:Ens]
let A = (power (power (union a b))) in
let B = (Separation A [x:Ens](EXT c:Ens | (IN c a)/\
(EXT d:Ens | (IN d b)/\(x==(orderedPair c d))))) in
Cases B of (exT_intro x _) => x end.
Theorem crossProd1 : (a,b,c,d:Ens)((IN c a)/\(IN d b))->
(IN (orderedPair c d) (power (power (union a b)))).
Proof.
Intros.
Induction H.
LetTac p := (power1 (orderedPair c d) (power (union a b))).
Apply (proj2 ? ? p).
Clear p.
Unfold sube.
Intros.
LetTac p := (power1 z (union a b)).
Apply (proj2 ? ? p).
Clear p.
Unfold sube.
Intros.
LetTac p := (union2 a b z0).
Apply (proj2 ? ? p).
Clear p.
Unfold orderedPair in H1.
LetTac p := (pair1 (single c) (pair c d) z).
Case ((proj1 ? ? p) H1).
Clear p.
Intros.
Rewrite H3 in H2.
LetTac p := (single1 c z0).
LetTac p1 := ((proj1 ? ? p) H2).
Rewrite <- p1 in H.
Auto.
Clear p.
Intros.
Rewrite H3 in H2.
LetTac p := (pair1 c d z0).
Case ((proj1 ? ? p) H2).
Clear p.
Intro.
Rewrite <- H4 in H.
Auto.
Intro.
Rewrite <- H4 in H0.
Auto.
Qed.
Theorem crossProd2 : (a,b,c:Ens)(IN c (crossProd a b))<->
(EXT a':Ens | (IN a' a)/\ (EXT b':Ens | (IN b' b)/\c==(orderedPair a' b'))).
Proof.
Intros.
Unfold crossProd.
LetTac q := (crossProd1 a b).
LetTac A := (power(power (union a b))).
LetTac B := (Separation A [x:Ens](EXT c:Ens | (IN c a)/\
(EXT d:Ens | (IN d b)/\(x==(orderedPair c d))))).
LetTac p := ((PI2 ? [x:Ens](y:Ens)
(IN y x)
<->(IN y A)
/\(EXT c:Ens |
(IN c a)/\(EXT d:Ens | (IN d b)/\y==(orderedPair c d))) B) c).
Unfold PI1 in p.
Constructor.
Intros.
LetTac p1 := (proj2 ? ? ((proj1 ? ? p) H)).
Auto.
Intros.
Apply (proj2 ? ? p).
Constructor.
Repeat Induction H.
Repeat Induction H0.
LetTac p1 := (q x x0).
Rewrite <- H1 in p1.
Apply p1.
Auto.
Auto.
Qed.
Definition isRelation : Ens -> Prop :=
[R:Ens](x:Ens)(IN x R)->(EXT a:Ens | (EXT b:Ens | x==(orderedPair a b))).
Definition related : Ens -> Ens -> Ens -> Prop :=
[a:Ens][R:Ens][b:Ens](IN (orderedPair a b) R).
Theorem related1 : (x,R:Ens)(EXT c:Ens | (related x R c)) ->
(IN x (sum (sum R))).
Proof.
Intros.
Unfold related in H.
Induction H.
Unfold orderedPair in H.
Apply (proj2 ? ? (sum1 x (sum R))).
Exists (single x).
Constructor.
Apply (proj2 ? ? (sum1 (single x) R)).
Exists (pair (single x) (pair x x0)).
Constructor.
Auto.
Apply pair2.
Apply single2.
Qed.
Theorem related2 : (x,R:Ens)(EXT c:Ens | (related c R x)) ->
(IN x (sum (sum R))).
Proof.
Intros.
Unfold related in H.
Induction H.
Unfold orderedPair in H.
Apply (proj2 ? ? (sum1 x (sum R))).
Exists (pair x0 x).
Constructor.
Apply (proj2 ? ? (sum1 (pair x0 x) R)).
Exists (pair (single x0) (pair x0 x)).
Constructor.
Auto.
Apply pair3.
Apply pair3.
Qed.
Definition domain : Ens -> Ens :=
[R:Ens]
let A = (sum (sum R)) in
let B = (Separation A [x:Ens](EXT c:Ens | (related x R c))) in
Cases B of (exT_intro x _) => x end.
Theorem domain1 : (x,R:Ens)(IN x (domain R))<->(EXT c:Ens | (related x R c)).
Proof.
Intros.
Unfold domain.
LetTac A := (sum (sum R)).
LetTac B := (Separation A [x:Ens](EXT c:Ens | (related x R c))).
LetTac p := (PI2 ? [x:Ens](y:Ens)(IN y x)<->(IN y A)/\(EXT c:Ens | (related y R c)) B).
Constructor.
Intros.
LetTac p1 := ((proj1 ? ? (p x)) H).
Apply (proj2 ? ? p1).
Intros.
Apply (proj2 ? ? (p x)).
Constructor.
Apply (related1 x R).
Auto.
Auto.
Qed.
Definition range : Ens -> Ens :=
[R:Ens]
let A = (sum (sum R)) in
let B = (Separation A [x:Ens](EXT c:Ens | (related c R x))) in
Cases B of (exT_intro x _) => x end.
Theorem range1 : (x,R:Ens)(IN x (range R))<->(EXT c:Ens | (related c R x)).
Proof.
Intros.
Unfold range.
LetTac A := (sum (sum R)).
LetTac B := (Separation A [x:Ens](EXT c:Ens | (related c R x))).
LetTac p := (PI2 ? [x:Ens](y:Ens)(IN y x)<->(IN y A)/\(EXT c:Ens | (related c R y)) B).
Constructor.
Intros.
LetTac p1 := ((proj1 ? ? (p x)) H).
Apply (proj2 ? ? p1).
Intros.
Apply (proj2 ? ? (p x)).
Constructor.
Apply (related2 x R).
Auto.
Auto.
Qed.
Theorem relations1 : (a,b,R:Ens)(isRelation R)/\(sube (domain R) b)/\
(sube (range R) a)->(IN R (power (crossProd b a))).
Proof.
Intros.
Induction H.
Induction H0.
Unfold isRelation in H.
Apply (proj2 ? ? (power1 R (crossProd b a))).
Unfold sube.
Intros.
Apply (proj2 ? ? (crossProd2 b a z)).
LetTac p := (H z H2).
Induction p.
Induction H3.
Exists x.
Constructor.
Apply H0.
Apply (proj2 ? ? (domain1 x R)).
Unfold related.
Exists x0.
Rewrite <- H3.
Auto.
Exists x0.
Constructor.
Apply H1.
Apply (proj2 ? ? (range1 x0 R)).
Exists x.
Unfold related.
Rewrite <- H3.
Auto.
Auto.
Qed.
Definition field : Ens -> Ens :=
[R:Ens](union (domain R) (range R)).
Definition isFunction : Ens -> Prop :=
[f:Ens](isRelation f)/\((x,y,z:Ens)((related x f y)/\(related x f z))->y==z).
Definition functions : Ens -> Ens -> Ens :=
[a:Ens][b:Ens]
let A = (power (crossProd b a)) in
let B = (Separation A [x:Ens](isFunction x)/\(domain x)==b/\(sube (range x) a))
in
Cases B of (exT_intro x _) => x end.
Theorem functions1 : (a,b,f:Ens)(IN f (functions a b))<->
((isFunction f)/\(domain f)==b/\(sube (range f) a)).
Proof.
Intros.
Unfold functions.
LetTac A := (power (crossProd b a)).
LetTac B := (Separation A [x:Ens](isFunction x)/\(domain x)==b/\(sube (range x) a)).
LetTac p := (PI2 ? [x:Ens](y:Ens)
(IN y x)
<->(IN y A)/\(isFunction y)/\(domain y)==b/\(sube (range y) a) B).
Unfold PI1 in p.
Constructor.
Intros.
LetTac p1 := ((proj1 ? ? (p f)) H).
Tauto.
Intros.
Apply (proj2 ? ? (p f)).
Constructor.
Apply (relations1 a b f).
Unfold isFunction in H.
Constructor.
Tauto.
Constructor.
Apply sube1.
Tauto.
Tauto.
Auto.
Qed.