THEOREM

*******

On any set x, there exists a function f: x --> x such that f(a)=a (the identity function on set x).

Formally stated in DC Proof notation: ALL(x):[Set(x) => EXIST(f):[Function(f,x,x) & ALL(a):[a e x => f(a)=a]]]

This theorem is usually presented as a "definition" in textbooks as it is thought to be so "intuitively obvious."

Here, we will not simply define this function, but actually prove its existence using the axioms of set theory.

By Dan Christensen

2022-11-17

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

Suppose...

1 Set(x)

Premise

Apply Cartesian Product Axiom

2 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

Cart Prod

3 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]

U Spec, 2

4 Set(x) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]

U Spec, 3

5 Set(x) & Set(x)

Join, 1, 1

6 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]

Detach, 4, 5

7 Set'(x2) & ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]

E Spec, 6

Define: x2

8 Set'(x2)

Split, 7

9 ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]

Split, 7

Apply Subset Axiom

10 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e x2 & a=b]]

Subset, 8

11 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e x2 & a=b]

E Spec, 10

Define: g

12 Set'(g)

Split, 11

13 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e x2 & a=b]

Split, 11

Apply Function Axiom

14 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)

=> [ALL(a1):ALL(b):[(a1,b) e gra => a1 e dom & b e cod]

& ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e gra]]

& ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod

=> [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 e dom & b e cod

=> [fun(a1)=b <=> (a1,b) e gra]]]]]

Function

15 ALL(cod):ALL(gra):[Set(x) & Set(cod) & Set'(gra)

=> [ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e cod]

& ALL(a1):[a1 e x => EXIST(b):[b e cod & (a1,b) e gra]]

& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod

=> [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

=> EXIST(fun):[Function(fun,x,cod) & ALL(a1):ALL(b):[a1 e x & b e cod

=> [fun(a1)=b <=> (a1,b) e gra]]]]]

U Spec, 14

16 ALL(gra):[Set(x) & Set(x) & Set'(gra)

=> [ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e x]

& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e gra]]

& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

=> [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

=> EXIST(fun):[Function(fun,x,x) & ALL(a1):ALL(b):[a1 e x & b e x

=> [fun(a1)=b <=> (a1,b) e gra]]]]]

U Spec, 15

17 Set(x) & Set(x) & Set'(g)

=> [ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]

& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]

& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]

=> EXIST(fun):[Function(fun,x,x) & ALL(a1):ALL(b):[a1 e x & b e x

=> [fun(a1)=b <=> (a1,b) e g]]]]

U Spec, 16

18 Set(x) & Set(x)

Join, 1, 1

19 Set(x) & Set(x) & Set'(g)

Join, 18, 12

Sufficient: For functionality of g

20 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]

& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]

& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]

=> EXIST(fun):[Function(fun,x,x) & ALL(a1):ALL(b):[a1 e x & b e x

=> [fun(a1)=b <=> (a1,b) e g]]]

Detach, 17, 19

Part 1

Prove: ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]

Suppose...

21 (t,u) e g

Premise

22 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]

U Spec, 13

23 (t,u) e g <=> (t,u) e x2 & t=u

U Spec, 22

24 [(t,u) e g => (t,u) e x2 & t=u]

& [(t,u) e x2 & t=u => (t,u) e g]

Iff-And, 23

25 (t,u) e g => (t,u) e x2 & t=u

Split, 24

26 (t,u) e x2 & t=u

Detach, 25, 21

27 (t,u) e x2

Split, 26

28 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]

U Spec, 9

29 (t,u) e x2 <=> t e x & u e x

U Spec, 28

30 [(t,u) e x2 => t e x & u e x]

& [t e x & u e x => (t,u) e x2]

Iff-And, 29

31 (t,u) e x2 => t e x & u e x

Split, 30

32 t e x & u e x

Detach, 31, 27

Part 1

As Required:

33 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]

4 Conclusion, 21

Part 2

Prove: ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]

Suppose...

34 t e x

Premise

35 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]

U Spec, 13

36 (t,t) e g <=> (t,t) e x2 & t=t

U Spec, 35

37 [(t,t) e g => (t,t) e x2 & t=t]

& [(t,t) e x2 & t=t => (t,t) e g]

Iff-And, 36

38 (t,t) e x2 & t=t => (t,t) e g

Split, 37

39 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]

U Spec, 9

40 (t,t) e x2 <=> t e x & t e x

U Spec, 39

41 [(t,t) e x2 => t e x & t e x]

& [t e x & t e x => (t,t) e x2]

Iff-And, 40

42 (t,t) e x2 => t e x & t e x

Split, 41

43 t e x & t e x => (t,t) e x2

Split, 41

44 t e x & t e x

Join, 34, 34

45 (t,t) e x2

Detach, 43, 44

46 t=t

Reflex

47 (t,t) e x2 & t=t

Join, 45, 46

48 (t,t) e g

Detach, 38, 47

49 t e x & (t,t) e g

Join, 34, 48

50 EXIST(b):[b e x & (t,b) e g]

E Gen, 49

Part 2

As Required:

51 ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]

4 Conclusion, 34

Part 3

Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x => [(a1,b1) e g & (a1,b2) e g => b1=b2]]

Suppose...

52 t e x & u e x & v e x

Premise

53 t e x

Split, 52

54 u e x

Split, 52

55 v e x

Split, 52

Prove: (t,u) e g & (t,v) e g => u=v

Suppose...

56 (t,u) e g & (t,v) e g

Premise

57 (t,u) e g

Split, 56

58 (t,v) e g

Split, 56

59 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]

U Spec, 13

60 (t,u) e g <=> (t,u) e x2 & t=u

U Spec, 59

61 [(t,u) e g => (t,u) e x2 & t=u]

& [(t,u) e x2 & t=u => (t,u) e g]

Iff-And, 60

62 (t,u) e g => (t,u) e x2 & t=u

Split, 61

63 (t,u) e x2 & t=u

Detach, 62, 57

64 t=u

Split, 63

65 (t,v) e g <=> (t,v) e x2 & t=v

U Spec, 59

66 [(t,v) e g => (t,v) e x2 & t=v]

& [(t,v) e x2 & t=v => (t,v) e g]

Iff-And, 65

67 (t,v) e g => (t,v) e x2 & t=v

Split, 66

68 (t,v) e x2 & t=v

Detach, 67, 58

69 t=v

Split, 68

70 u=v

Substitute, 64, 69

As Required:

71 (t,u) e g & (t,v) e g => u=v

4 Conclusion, 56

Part 3

As Required:

72 ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x => [(a1,b1) e g & (a1,b2) e g => b1=b2]]

4 Conclusion, 52

Joining results...

73 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]

& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]

Join, 33, 51

74 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]

& ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e g]]

& ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x => [(a1,b1) e g & (a1,b2) e g => b1=b2]]

Join, 73, 72

75 EXIST(fun):[Function(fun,x,x) & ALL(a1):ALL(b):[a1 e x & b e x

=> [fun(a1)=b <=> (a1,b) e g]]]

Detach, 20, 74

76 Function(f,x,x) & ALL(a1):ALL(b):[a1 e x & b e x

=> [f(a1)=b <=> (a1,b) e g]]

E Spec, 75

We have function f: x --> x

As Required:

77 Function(f,x,x)

Split, 76

Function f defined in terms of its graph set:

78 ALL(a1):ALL(b):[a1 e x & b e x

=> [f(a1)=b <=> (a1,b) e g]]

Split, 76

Prove: ALL(a):[a e x => f(a)=a]

Suppose...

79 t e x

Premise

80 t e x => EXIST(b):[b e x & (t,b) e g]

U Spec, 51

81 EXIST(b):[b e x & (t,b) e g]

Detach, 80, 79

82 u e x & (t,u) e g

E Spec, 81

83 u e x

Split, 82

84 (t,u) e g

Split, 82

85 ALL(b):[t e x & b e x

=> [f(t)=b <=> (t,b) e g]]

U Spec, 78

86 t e x & u e x

=> [f(t)=u <=> (t,u) e g]

U Spec, 85

87 t e x & u e x

Join, 79, 83

88 f(t)=u <=> (t,u) e g

Detach, 86, 87

89 [f(t)=u => (t,u) e g] & [(t,u) e g => f(t)=u]

Iff-And, 88

90 (t,u) e g => f(t)=u

Split, 89

91 f(t)=u

Detach, 90, 84

92 ALL(b):[(t,b) e g <=> (t,b) e x2 & t=b]

U Spec, 13

93 (t,u) e g <=> (t,u) e x2 & t=u

U Spec, 92

94 [(t,u) e g => (t,u) e x2 & t=u]

& [(t,u) e x2 & t=u => (t,u) e g]

Iff-And, 93

95 (t,u) e g => (t,u) e x2 & t=u

Split, 94

96 (t,u) e x2 & t=u

Detach, 95, 84

97 t=u

Split, 96

98 f(t)=t

Substitute, 97, 91

As Required:

99 ALL(a):[a e x => f(a)=a]

4 Conclusion, 79

100 Function(f,x,x) & ALL(a):[a e x => f(a)=a]

Join, 77, 99

As Required:

101 ALL(x):[Set(x)

=> EXIST(f):[Function(f,x,x) & ALL(a):[a e x => f(a)=a]]]

4 Conclusion, 1