THEOREM

*******

 

There exists the set of all fisons = {{0}, {0,1}, {0,1,2} ...} and a bijection f: n --> fisons where n is the set

of natural numbers.

 

Formally:

 

     EXIST(fisons):EXIST(f):[Set(fisons)

     & ALL(a):[a e fisons

     <=> Set(a) & ALL(b):[b e a => b e n]

     & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]

 

     & ALL(a):[a e n => f(a) e fisons]                           (f(x) = {0, 1, 2, ... x})

     & ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]   (f is surjective)

     & ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]]      (f is injective)

 

OUTLINE OF PROOF

****************

 

Lines

 

5-52     Construct the set of all fisons

 

53-64    Construct the set f

 

65-309   Prove f is a function mapping n to the set of all fisons

 

310-328  Prove f is surjective

 

343-408  Prove f is injective

 

 

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 proof-checker available at

http://www.dcproof.com

 

 

AXIOMS

******

 

1     Set(n)

      Axiom

 

 

Define: <= on n

 

2     ALL(a):[a e n => a<=a]

      Axiom

 

3     ALL(a):ALL(b):[a e n & b e n => [a<=b & b<=a => a=b]]

      Axiom

 

Function Axiom (single variable)

 

4     ALL(f):ALL(a):ALL(b):[Set'(f) & Set(a) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e f => c e a & d e b]

    & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]

      Axiom

 

 

PROOF

*****

 

Construct the set of all fisons

 

Apply Power Set Axiom

 

5     ALL(a):[Set(a) => EXIST(b):[Set(b)

    & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]

      Power Set

 

6     Set(n) => EXIST(b):[Set(b)

    & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e n]]]

      U Spec, 5

 

7     EXIST(b):[Set(b)

    & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e n]]]

      Detach, 6, 1

 

Define: pn

 

Power set of n

 

8     Set(pn)

    & ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      E Spec, 7

 

9     Set(pn)

      Split, 8

 

10   ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      Split, 8

 

Apply Subset Axiom

 

11   EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]]

      Subset, 9

 

Define: fisons

 

12   Set(fisons) & ALL(a):[a e fisons <=> a e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]

      E Spec, 11

 

13   Set(fisons)

      Split, 12

 

14   ALL(a):[a e fisons <=> a e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]

      Split, 12

 

   

    Suppose...

 

      15   x e fisons

            Premise

 

      16   x e fisons <=> x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            U Spec, 14

 

      17   [x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]]

         & [x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons]

            Iff-And, 16

 

      18   x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Split, 17

 

      19   x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons

            Split, 17

 

      20   x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Detach, 18, 15

 

      21   x e pn

            Split, 20

 

      22   EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Split, 20

 

      23   x e pn <=> Set(x) & ALL(d):[d e x => d e n]

            U Spec, 10

 

      24   [x e pn => Set(x) & ALL(d):[d e x => d e n]]

         & [Set(x) & ALL(d):[d e x => d e n] => x e pn]

            Iff-And, 23

 

      25   x e pn => Set(x) & ALL(d):[d e x => d e n]

            Split, 24

 

      26   Set(x) & ALL(d):[d e x => d e n] => x e pn

            Split, 24

 

      27   Set(x) & ALL(d):[d e x => d e n]

            Detach, 25, 21

 

      28   Set(x)

            Split, 27

 

      29   ALL(d):[d e x => d e n]

            Split, 27

 

      30   ALL(b):[b e x => b e n]

            Rename, 29

 

      31   Set(x) & ALL(b):[b e x => b e n]

            Join, 28, 30

 

      32   Set(x) & ALL(b):[b e x => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Join, 31, 22

 

33   ALL(a):[a e fisons

    => Set(a) & ALL(b):[b e a => b e n]

    & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]

      4 Conclusion, 15

 

   

    Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]

           & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]

           => a e fisons]

   

    Suppose...

 

      34   Set(x) & ALL(b):[b e x => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Premise

 

      35   Set(x)

            Split, 34

 

      36   ALL(b):[b e x => b e n]

            Split, 34

 

      37   EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Split, 34

 

      38   x e fisons <=> x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            U Spec, 14

 

      39   [x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]]

         & [x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons]

            Iff-And, 38

 

      40   x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Split, 39

 

    Sufficient: For x e fisons

 

      41   x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons

            Split, 39

 

      42   x e pn <=> Set(x) & ALL(d):[d e x => d e n]

            U Spec, 10

 

      43   [x e pn => Set(x) & ALL(d):[d e x => d e n]]

         & [Set(x) & ALL(d):[d e x => d e n] => x e pn]

            Iff-And, 42

 

      44   x e pn => Set(x) & ALL(d):[d e x => d e n]

            Split, 43

 

    As Required:

 

      45   Set(x) & ALL(d):[d e x => d e n] => x e pn

            Split, 43

 

      46   Set(x) & ALL(b):[b e x => b e n]

            Join, 35, 36

 

      47   x e pn

            Detach, 45, 46

 

      48   x e pn

         & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]

            Join, 47, 37

 

      49   x e fisons

            Detach, 41, 48

 

As Required:

 

50   ALL(a):[Set(a) & ALL(b):[b e a => b e n]

    & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]

    => a e fisons]

      4 Conclusion, 34

 

51   ALL(a):[[a e fisons

    => Set(a) & ALL(b):[b e a => b e n]

    & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]] & [Set(a) & ALL(b):[b e a => b e n]

    & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]

    => a e fisons]]

      Join, 33, 50

 

As Required:

 

52   ALL(a):[a e fisons

    <=> Set(a) & ALL(b):[b e a => b e n]

    & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]

      Iff-And, 51

 

 

Construct the set f

 

Apply Cartesian Product Axiom

 

53   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

 

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

      U Spec, 53

 

55   Set(n) & Set(fisons) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e fisons]]

      U Spec, 54

 

56   Set(n) & Set(fisons)

      Join, 1, 13

 

57   EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e fisons]]

      Detach, 55, 56

 

Define: nf   (n x fisons)

 

58   Set'(nf) & ALL(c1):ALL(c2):[(c1,c2) e nf <=> c1 e n & c2 e fisons]

      E Spec, 57

 

59   Set'(nf)

      Split, 58

 

60   ALL(c1):ALL(c2):[(c1,c2) e nf <=> c1 e n & c2 e fisons]

      Split, 58

 

Apply Subset Axiom

 

61   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e nf & ALL(c):[c e n => [c e b <=> c<=a]]]]

      Subset, 59

 

Define: f

 

62   Set'(f) & ALL(a):ALL(b):[(a,b) e f <=> (a,b) e nf & ALL(c):[c e n => [c e b <=> c<=a]]]

      E Spec, 61

 

63   Set'(f)

      Split, 62

 

64   ALL(a):ALL(b):[(a,b) e f <=> (a,b) e nf & ALL(c):[c e n => [c e b <=> c<=a]]]

      Split, 62

 

 

Prove f is a function mapping n to the set of all fisons

 

Apply the Axiom of Functionality (one variable)

 

65   ALL(a):ALL(b):[Set'(f) & Set(a) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e f => c e a & d e b]

    & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]

      U Spec, 4

 

66   ALL(b):[Set'(f) & Set(n) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e f => c e n & d e b]

    & ALL(c):[c e n => EXIST(d):[d e b & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e n & d e b => [d=f(c) <=> (c,d) e f]]]]

      U Spec, 65

 

67   Set'(f) & Set(n) & Set(fisons)

    => [ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]

    & ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e n & d e fisons => [d=f(c) <=> (c,d) e f]]]

      U Spec, 66

 

68   Set'(f) & Set(n)

      Join, 63, 1

 

69   Set'(f) & Set(n) & Set(fisons)

      Join, 68, 13

 

Sufficient: For functionality of f

 

70   ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]

    & ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e n & d e fisons => [d=f(c) <=> (c,d) e f]]

      Detach, 67, 69

 

   

    Prove: ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]

   

    Suppose...

 

      71   (x,y) e f

            Premise

 

      72   ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]

            U Spec, 64

 

      73   (x,y) e f <=> (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            U Spec, 72

 

      74   [(x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]]

         & [(x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f]

            Iff-And, 73

 

      75   (x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            Split, 74

 

      76   (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f

            Split, 74

 

      77   (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            Detach, 75, 71

 

      78   (x,y) e nf

            Split, 77

 

      79   ALL(c):[c e n => [c e y <=> c<=x]]

            Split, 77

 

      80   ALL(c2):[(x,c2) e nf <=> x e n & c2 e fisons]

            U Spec, 60

 

      81   (x,y) e nf <=> x e n & y e fisons

            U Spec, 80

 

      82   [(x,y) e nf => x e n & y e fisons]

         & [x e n & y e fisons => (x,y) e nf]

            Iff-And, 81

 

      83   (x,y) e nf => x e n & y e fisons

            Split, 82

 

      84   x e n & y e fisons => (x,y) e nf

            Split, 82

 

      85   x e n & y e fisons

            Detach, 83, 78

 

Part 1

 

As Required:

 

86   ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]

      4 Conclusion, 71

 

   

    Prove: ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]

   

    Suppose...

 

      87   x e n

            Premise

 

      88   EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & a<=x]]

            Subset, 1

 

    Define: y

 

      89   Set(y) & ALL(a):[a e y <=> a e n & a<=x]

            E Spec, 88

 

      90   Set(y)

            Split, 89

 

      91   ALL(a):[a e y <=> a e n & a<=x]

            Split, 89

 

      92   y e fisons

         <=> Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            U Spec, 52

 

      93   [y e fisons => Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]]

         & [Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons]

            Iff-And, 92

 

      94   y e fisons => Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            Split, 93

 

    Sufficient: For y e fisons

 

      95   Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons

            Split, 93

 

        

         Prove: ALL(b):[b e y => b e n]

        

         Suppose...

 

            96   z e y

                  Premise

 

            97   z e y <=> z e n & z<=x

                  U Spec, 91

 

            98   [z e y => z e n & z<=x] & [z e n & z<=x => z e y]

                  Iff-And, 97

 

            99   z e y => z e n & z<=x

                  Split, 98

 

            100  z e n & z<=x => z e y

                  Split, 98

 

            101  z e n & z<=x

                  Detach, 99, 96

 

            102  z e n

                  Split, 101

 

    As Required:

 

      103  ALL(b):[b e y => b e n]

            4 Conclusion, 96

 

            104  z e n

                  Premise

 

                  105  z e y

                        Premise

 

                  106  z e y <=> z e n & z<=x

                        U Spec, 91

 

                  107  [z e y => z e n & z<=x] & [z e n & z<=x => z e y]

                        Iff-And, 106

 

                  108  z e y => z e n & z<=x

                        Split, 107

 

                  109  z e n & z<=x => z e y

                        Split, 107

 

                  110  z e n & z<=x

                        Detach, 108, 105

 

                  111  z e n

                        Split, 110

 

                  112  z<=x

                        Split, 110

 

            113  z e y => z<=x

                  4 Conclusion, 105

 

                  114  z<=x

                        Premise

 

                  115  z e y <=> z e n & z<=x

                        U Spec, 91

 

                  116  [z e y => z e n & z<=x] & [z e n & z<=x => z e y]

                        Iff-And, 115

 

                  117  z e y => z e n & z<=x

                        Split, 116

 

                  118  z e n & z<=x => z e y

                        Split, 116

 

                  119  z e n & z<=x

                        Join, 104, 114

 

                  120  z e y

                        Detach, 118, 119

 

            121  z<=x => z e y

                  4 Conclusion, 114

 

            122  [z e y => z<=x] & [z<=x => z e y]

                  Join, 113, 121

 

            123  z e y <=> z<=x

                  Iff-And, 122

 

    As Required:

 

      124  ALL(c):[c e n => [c e y <=> c<=x]]

            4 Conclusion, 104

 

      125  x e n & ALL(c):[c e n => [c e y <=> c<=x]]

            Join, 87, 124

 

      126  EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            E Gen, 125

 

      127  Set(y) & ALL(b):[b e y => b e n]

            Join, 90, 103

 

      128  Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            Join, 127, 126

 

      129  y e fisons

            Detach, 95, 128

 

      130  ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]

            U Spec, 64

 

      131  ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]

            U Spec, 64

 

      132  (x,y) e f <=> (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            U Spec, 131

 

      133  [(x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]]

         & [(x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f]

            Iff-And, 132

 

      134  (x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            Split, 133

 

    Sufficient:

 

      135  (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f

            Split, 133

 

      136  ALL(c2):[(x,c2) e nf <=> x e n & c2 e fisons]

            U Spec, 60

 

      137  (x,y) e nf <=> x e n & y e fisons

            U Spec, 136

 

      138  [(x,y) e nf => x e n & y e fisons]

         & [x e n & y e fisons => (x,y) e nf]

            Iff-And, 137

 

      139  (x,y) e nf => x e n & y e fisons

            Split, 138

 

      140  x e n & y e fisons => (x,y) e nf

            Split, 138

 

      141  x e n & y e fisons

            Join, 87, 129

 

      142  (x,y) e nf

            Detach, 140, 141

 

            143  z e n

                  Premise

 

            144  z e y <=> z e n & z<=x

                  U Spec, 91

 

            145  [z e y => z e n & z<=x] & [z e n & z<=x => z e y]

                  Iff-And, 144

 

            146  z e y => z e n & z<=x

                  Split, 145

 

            147  z e n & z<=x => z e y

                  Split, 145

 

                  148  z e y

                        Premise

 

                  149  z e n & z<=x

                        Detach, 146, 148

 

                  150  z e n

                        Split, 149

 

                  151  z<=x

                        Split, 149

 

            152  z e y => z<=x

                  4 Conclusion, 148

 

                  153  z<=x

                        Premise

 

                  154  z e n & z<=x

                        Join, 143, 153

 

                  155  z e y

                        Detach, 147, 154

 

            156  z<=x => z e y

                  4 Conclusion, 153

 

            157  [z e y => z<=x] & [z<=x => z e y]

                  Join, 152, 156

 

            158  z e y <=> z<=x

                  Iff-And, 157

 

      159  ALL(c):[c e n => [c e y <=> c<=x]]

            4 Conclusion, 143

 

      160  (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            Join, 142, 159

 

      161  (x,y) e f

            Detach, 135, 160

 

      162  y e fisons & (x,y) e f

            Join, 129, 161

 

      163  EXIST(d):[d e fisons & (x,d) e f]

            E Gen, 162

 

Part 2

 

As Required:

 

164  ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]

      4 Conclusion, 87

 

   

    Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

   

    Suppose...

 

      165  (x,y1) e f & (x,y2) e f

            Premise

 

      166  (x,y1) e f

            Split, 165

 

      167  (x,y2) e f

            Split, 165

 

      168  ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]

            U Spec, 64

 

      169  (x,y1) e f <=> (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]

            U Spec, 168

 

      170  [(x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]]

         & [(x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f]

            Iff-And, 169

 

      171  (x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]

            Split, 170

 

      172  (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f

            Split, 170

 

      173  (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]

            Detach, 171, 166

 

      174  (x,y1) e nf

            Split, 173

 

      175  ALL(c):[c e n => [c e y1 <=> c<=x]]

            Split, 173

 

      176  ALL(c2):[(x,c2) e nf <=> x e n & c2 e fisons]

            U Spec, 60

 

      177  (x,y1) e nf <=> x e n & y1 e fisons

            U Spec, 176

 

      178  [(x,y1) e nf => x e n & y1 e fisons]

         & [x e n & y1 e fisons => (x,y1) e nf]

            Iff-And, 177

 

      179  (x,y1) e nf => x e n & y1 e fisons

            Split, 178

 

      180  x e n & y1 e fisons => (x,y1) e nf

            Split, 178

 

      181  x e n & y1 e fisons

            Detach, 179, 174

 

      182  x e n

            Split, 181

 

      183  y1 e fisons

            Split, 181

 

      184  (x,y2) e f <=> (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]

            U Spec, 168

 

      185  [(x,y2) e f => (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]]

         & [(x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]] => (x,y2) e f]

            Iff-And, 184

 

      186  (x,y2) e f => (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]

            Split, 185

 

      187  (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]] => (x,y2) e f

            Split, 185

 

      188  (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]

            Detach, 186, 167

 

      189  (x,y2) e nf

            Split, 188

 

      190  ALL(c):[c e n => [c e y2 <=> c<=x]]

            Split, 188

 

      191  (x,y2) e nf <=> x e n & y2 e fisons

            U Spec, 176

 

      192  [(x,y2) e nf => x e n & y2 e fisons]

         & [x e n & y2 e fisons => (x,y2) e nf]

            Iff-And, 191

 

      193  (x,y2) e nf => x e n & y2 e fisons

            Split, 192

 

      194  x e n & y2 e fisons => (x,y2) e nf

            Split, 192

 

      195  x e n & y2 e fisons

            Detach, 193, 189

 

      196  x e n

            Split, 195

 

      197  y2 e fisons

            Split, 195

 

      198  (x,y1) e f <=> (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]

            U Spec, 168

 

      199  [(x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]]

         & [(x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f]

            Iff-And, 198

 

      200  (x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]

            Split, 199

 

      201  (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f

            Split, 199

 

      202  (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]

            Detach, 200, 166

 

      203  (x,y1) e nf

            Split, 202

 

      204  ALL(c):[c e n => [c e y1 <=> c<=x]]

            Split, 202

 

      205  ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]

            Set Equality

 

      206  ALL(b):[Set(y1) & Set(b) => [y1=b <=> ALL(c):[c e y1 <=> c e b]]]

            U Spec, 205

 

      207  Set(y1) & Set(y2) => [y1=y2 <=> ALL(c):[c e y1 <=> c e y2]]

            U Spec, 206

 

      208  y1 e fisons

         <=> Set(y1) & ALL(b):[b e y1 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]

            U Spec, 52

 

      209  [y1 e fisons => Set(y1) & ALL(b):[b e y1 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]]

         & [Set(y1) & ALL(b):[b e y1 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]] => y1 e fisons]

            Iff-And, 208

 

      210  y1 e fisons => Set(y1) & ALL(b):[b e y1 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]

            Split, 209

 

      211  Set(y1) & ALL(b):[b e y1 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]] => y1 e fisons

            Split, 209

 

      212  Set(y1) & ALL(b):[b e y1 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]

            Detach, 210, 183

 

      213  Set(y1)

            Split, 212

 

      214  ALL(b):[b e y1 => b e n]

            Split, 212

 

      215  EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]

            Split, 212

 

      216  y2 e fisons

         <=> Set(y2) & ALL(b):[b e y2 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]

            U Spec, 52

 

      217  [y2 e fisons => Set(y2) & ALL(b):[b e y2 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]]

         & [Set(y2) & ALL(b):[b e y2 => b e n]

        & EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]] => y2 e fisons]

            Iff-And, 216

 

      218  y2 e fisons => Set(y2) & ALL(b):[b e y2 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]

            Split, 217

 

      219  Set(y2) & ALL(b):[b e y2 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]] => y2 e fisons

            Split, 217

 

      220  Set(y2) & ALL(b):[b e y2 => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]

            Detach, 218, 197

 

      221  Set(y2)

            Split, 220

 

      222  ALL(b):[b e y2 => b e n]

            Split, 220

 

      223  EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]

            Split, 220

 

      224  Set(y1) & Set(y2)

            Join, 213, 221

 

      225  y1=y2 <=> ALL(c):[c e y1 <=> c e y2]

            Detach, 207, 224

 

      226  [y1=y2 => ALL(c):[c e y1 <=> c e y2]]

         & [ALL(c):[c e y1 <=> c e y2] => y1=y2]

            Iff-And, 225

 

      227  y1=y2 => ALL(c):[c e y1 <=> c e y2]

            Split, 226

 

    Sufficient: y1=y2

 

      228  ALL(c):[c e y1 <=> c e y2] => y1=y2

            Split, 226

 

        

         Prove: ALL(c):[c e y1 => c e y2]

        

         Suppose...

 

            229  z e y1

                  Premise

 

            230  z e y1 => z e n

                  U Spec, 214

 

            231  z e n

                  Detach, 230, 229

 

            232  z e n => [z e y1 <=> z<=x]

                  U Spec, 175

 

            233  z e y1 <=> z<=x

                  Detach, 232, 231

 

            234  [z e y1 => z<=x] & [z<=x => z e y1]

                  Iff-And, 233

 

            235  z e y1 => z<=x

                  Split, 234

 

            236  z<=x => z e y1

                  Split, 234

 

            237  z<=x

                  Detach, 235, 229

 

            238  z e n => [z e y2 <=> z<=x]

                  U Spec, 190

 

            239  z e y2 <=> z<=x

                  Detach, 238, 231

 

            240  [z e y2 => z<=x] & [z<=x => z e y2]

                  Iff-And, 239

 

            241  z e y2 => z<=x

                  Split, 240

 

            242  z<=x => z e y2

                  Split, 240

 

            243  z e y2

                  Detach, 242, 237

 

    As Required:

 

      244  ALL(c):[c e y1 => c e y2]

            4 Conclusion, 229

 

        

         Prove: ALL(c):[c e y2 => c e y1]

        

         Suppose...

 

            245  z e y2

                  Premise

 

            246  z e y2 => z e n

                  U Spec, 222

 

            247  z e n

                  Detach, 246, 245

 

            248  z e n => [z e y2 <=> z<=x]

                  U Spec, 190

 

            249  z e y2 <=> z<=x

                  Detach, 248, 247

 

            250  [z e y2 => z<=x] & [z<=x => z e y2]

                  Iff-And, 249

 

            251  z e y2 => z<=x

                  Split, 250

 

            252  z<=x => z e y2

                  Split, 250

 

            253  z<=x

                  Detach, 251, 245

 

            254  z e n => [z e y1 <=> z<=x]

                  U Spec, 204

 

            255  z e y1 <=> z<=x

                  Detach, 254, 247

 

            256  [z e y1 => z<=x] & [z<=x => z e y1]

                  Iff-And, 255

 

            257  z e y1 => z<=x

                  Split, 256

 

            258  z<=x => z e y1

                  Split, 256

 

            259  z e y1

                  Detach, 258, 253

 

    As Required:

 

      260  ALL(c):[c e y2 => c e y1]

            4 Conclusion, 245

 

      261  ALL(c):[[c e y1 => c e y2] & [c e y2 => c e y1]]

            Join, 244, 260

 

      262  ALL(c):[c e y1 <=> c e y2]

            Iff-And, 261

 

      263  y1=y2

            Detach, 228, 262

 

Part 3

 

As Required:

 

264  ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

      4 Conclusion, 165

 

265  ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]

    & ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]

      Join, 86, 164

 

266  ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]

    & ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

      Join, 265, 264

 

As Required:

 

f is a function mapping the set n to the set of fisons

 

267  ALL(c):ALL(d):[c e n & d e fisons => [d=f(c) <=> (c,d) e f]]

      Detach, 70, 266

 

      268  x e n

            Premise

 

      269  x e n => EXIST(d):[d e fisons & (x,d) e f]

            U Spec, 164

 

      270  EXIST(d):[d e fisons & (x,d) e f]

            Detach, 269, 268

 

      271  y e fisons & (x,y) e f

            E Spec, 270

 

      272  y e fisons

            Split, 271

 

      273  (x,y) e f

            Split, 271

 

      274  ALL(d):[x e n & d e fisons => [d=f(x) <=> (x,d) e f]]

            U Spec, 267

 

      275  x e n & y e fisons => [y=f(x) <=> (x,y) e f]

            U Spec, 274

 

      276  x e n & y e fisons

            Join, 268, 272

 

      277  y=f(x) <=> (x,y) e f

            Detach, 275, 276

 

      278  [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]

            Iff-And, 277

 

      279  y=f(x) => (x,y) e f

            Split, 278

 

      280  (x,y) e f => y=f(x)

            Split, 278

 

      281  y=f(x)

            Detach, 280, 273

 

      282  f(x) e fisons

            Substitute, 281, 272

 

As Required:

 

283  ALL(a):[a e n => f(a) e fisons]

      4 Conclusion, 268

 

   

    Prove: ALL(a):[a e n

           => f(a) e fisons

           & ALL(c):[c e n => [c e f(a) <=> c<=a]]]

   

    Suppose...

 

      284  x e n

            Premise

 

      285  x e n => EXIST(d):[d e fisons & (x,d) e f]

            U Spec, 164

 

      286  EXIST(d):[d e fisons & (x,d) e f]

            Detach, 285, 284

 

      287  y e fisons & (x,y) e f

            E Spec, 286

 

      288  y e fisons

            Split, 287

 

      289  (x,y) e f

            Split, 287

 

      290  ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]

            U Spec, 64

 

      291  (x,y) e f <=> (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            U Spec, 290

 

      292  [(x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]]

         & [(x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f]

            Iff-And, 291

 

      293  (x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            Split, 292

 

      294  (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f

            Split, 292

 

      295  (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]

            Detach, 293, 289

 

      296  (x,y) e nf

            Split, 295

 

      297  ALL(c):[c e n => [c e y <=> c<=x]]

            Split, 295

 

      298  ALL(d):[x e n & d e fisons => [d=f(x) <=> (x,d) e f]]

            U Spec, 267

 

      299  x e n & y e fisons => [y=f(x) <=> (x,y) e f]

            U Spec, 298

 

      300  x e n & y e fisons

            Join, 284, 288

 

      301  y=f(x) <=> (x,y) e f

            Detach, 299, 300

 

      302  [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]

            Iff-And, 301

 

      303  y=f(x) => (x,y) e f

            Split, 302

 

      304  (x,y) e f => y=f(x)

            Split, 302

 

      305  y=f(x)

            Detach, 304, 289

 

      306  ALL(c):[c e n => [c e f(x) <=> c<=x]]

            Substitute, 305, 297

 

      307  f(x) e fisons

            Substitute, 305, 288

 

      308  f(x) e fisons

         & ALL(c):[c e n => [c e f(x) <=> c<=x]]

            Join, 307, 306

 

As Required:

 

309  ALL(a):[a e n

    => f(a) e fisons

    & ALL(c):[c e n => [c e f(a) <=> c<=a]]]

      4 Conclusion, 284

 

   

    Prove: f is surjective

   

    Suppose...

 

      310  y e fisons

            Premise

 

      311  y e fisons

         <=> Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            U Spec, 52

 

      312  [y e fisons => Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]]

         & [Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons]

            Iff-And, 311

 

      313  y e fisons => Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            Split, 312

 

      314  Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons

            Split, 312

 

      315  Set(y) & ALL(b):[b e y => b e n]

         & EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            Detach, 313, 310

 

      316  Set(y)

            Split, 315

 

      317  ALL(b):[b e y => b e n]

            Split, 315

 

      318  EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]

            Split, 315

 

      319  z e n & ALL(c):[c e n => [c e y <=> c<=z]]

            E Spec, 318

 

    Define: z

 

      320  z e n

            Split, 319

 

      321  ALL(c):[c e n => [c e y <=> c<=z]]

            Split, 319

 

      322  z e n

         => f(z) e fisons

         & ALL(c):[c e n => [c e f(z) <=> c<=z]]

            U Spec, 309

 

      323  f(z) e fisons

         & ALL(c):[c e n => [c e f(z) <=> c<=z]]

            Detach, 322, 320

 

      324  f(z) e fisons

            Split, 323

 

      325  ALL(c):[c e n => [c e f(z) <=> c<=z]]

            Split, 323

 

      326  z e n & f(z) e fisons

            Join, 320, 324

 

      327  EXIST(b):[b e n & f(b) e fisons]

            E Gen, 326

 

f is surjective

 

As Required:

 

328  ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]

      4 Conclusion, 310

 

   

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

   

    Suppose...

 

      329  x e n

            Premise

 

      330  x e n

         => f(x) e fisons

         & ALL(c):[c e n => [c e f(x) <=> c<=x]]

            U Spec, 309

 

      331  f(x) e fisons

         & ALL(c):[c e n => [c e f(x) <=> c<=x]]

            Detach, 330, 329

 

      332  f(x) e fisons

            Split, 331

 

      333  ALL(c):[c e n => [c e f(x) <=> c<=x]]

            Split, 331

 

      334  x e n => [x e f(x) <=> x<=x]

            U Spec, 333

 

      335  x e f(x) <=> x<=x

            Detach, 334, 329

 

      336  [x e f(x) => x<=x] & [x<=x => x e f(x)]

            Iff-And, 335

 

      337  x e f(x) => x<=x

            Split, 336

 

      338  x<=x => x e f(x)

            Split, 336

 

      339  x e n => x<=x

            U Spec, 2

 

      340  x<=x

            Detach, 339, 329

 

      341  x e f(x)

            Detach, 338, 340

 

As Required:

 

342  ALL(a):[a e n => a e f(a)]

      4 Conclusion, 329

 

   

    Prove: f is injective

   

    Suppose...

 

      343  x1 e n & x2 e n

            Premise

 

      344  x1 e n

            Split, 343

 

      345  x2 e n

            Split, 343

 

      346  x1 e n => x1 e f(x1)

            U Spec, 342

 

      347  x1 e f(x1)

            Detach, 346, 344

 

      348  x2 e n => x2 e f(x2)

            U Spec, 342

 

      349  x2 e f(x2)

            Detach, 348, 345

 

      350  x1 e n

         => f(x1) e fisons

         & ALL(c):[c e n => [c e f(x1) <=> c<=x1]]

            U Spec, 309

 

      351  f(x1) e fisons

         & ALL(c):[c e n => [c e f(x1) <=> c<=x1]]

            Detach, 350, 344

 

      352  f(x1) e fisons

            Split, 351

 

      353  ALL(c):[c e n => [c e f(x1) <=> c<=x1]]

            Split, 351

 

      354  x2 e n

         => f(x2) e fisons

         & ALL(c):[c e n => [c e f(x2) <=> c<=x2]]

            U Spec, 309

 

      355  f(x2) e fisons

         & ALL(c):[c e n => [c e f(x2) <=> c<=x2]]

            Detach, 354, 345

 

      356  f(x2) e fisons

            Split, 355

 

      357  ALL(c):[c e n => [c e f(x2) <=> c<=x2]]

            Split, 355

 

        

         Prove: f(x1)=f(x2) => x1=x2

        

         Suppose...

 

            358  f(x1)=f(x2)

                  Premise

 

            359  ALL(c):[c e n => [c e f(x1) <=> c<=x2]]

                  Substitute, 358, 357

 

            360  x1 e n => [x1 e f(x1) <=> x1<=x2]

                  U Spec, 359

 

            361  x1 e f(x1) <=> x1<=x2

                  Detach, 360, 344

 

            362  [x1 e f(x1) => x1<=x2] & [x1<=x2 => x1 e f(x1)]

                  Iff-And, 361

 

            363  x1 e f(x1) => x1<=x2

                  Split, 362

 

            364  x1<=x2 => x1 e f(x1)

                  Split, 362

 

            365  x1<=x2

                  Detach, 363, 347

 

            366  x2 e n => [x2 e f(x1) <=> x2<=x1]

                  U Spec, 353

 

            367  x2 e f(x1) <=> x2<=x1

                  Detach, 366, 345

 

            368  [x2 e f(x1) => x2<=x1] & [x2<=x1 => x2 e f(x1)]

                  Iff-And, 367

 

            369  x2 e f(x1) => x2<=x1

                  Split, 368

 

            370  x2<=x1 => x2 e f(x1)

                  Split, 368

 

            371  ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]

                  Set Equality

 

            372  ALL(b):[Set(f(x1)) & Set(b) => [f(x1)=b <=> ALL(c):[c e f(x1) <=> c e b]]]

                  U Spec, 371

 

            373  Set(f(x1)) & Set(f(x2)) => [f(x1)=f(x2) <=> ALL(c):[c e f(x1) <=> c e f(x2)]]

                  U Spec, 372

 

            374  f(x1) e fisons

             <=> Set(f(x1)) & ALL(b):[b e f(x1) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]

                  U Spec, 52

 

            375  [f(x1) e fisons => Set(f(x1)) & ALL(b):[b e f(x1) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]]

             & [Set(f(x1)) & ALL(b):[b e f(x1) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]] => f(x1) e fisons]

                  Iff-And, 374

 

            376  f(x1) e fisons => Set(f(x1)) & ALL(b):[b e f(x1) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]

                  Split, 375

 

            377  Set(f(x1)) & ALL(b):[b e f(x1) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]] => f(x1) e fisons

                  Split, 375

 

            378  Set(f(x1)) & ALL(b):[b e f(x1) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]

                  Detach, 376, 352

 

            379  Set(f(x1))

                  Split, 378

 

            380  ALL(b):[b e f(x1) => b e n]

                  Split, 378

 

            381  EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]

                  Split, 378

 

            382  f(x2) e fisons

             <=> Set(f(x2)) & ALL(b):[b e f(x2) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]

                  U Spec, 52

 

            383  [f(x2) e fisons => Set(f(x2)) & ALL(b):[b e f(x2) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]]

             & [Set(f(x2)) & ALL(b):[b e f(x2) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]] => f(x2) e fisons]

                  Iff-And, 382

 

            384  f(x2) e fisons => Set(f(x2)) & ALL(b):[b e f(x2) => b e n]

             & EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]

                  Split, 383

 

            385  Set(