Term definitions:


*sing(x1) = {x2|x2 = x1}

*one = {x1|(Ex2.x1 = *sing(x2))}

*union(x1,x2) = {x3|x3 E x1 v x3 E x2}

*s(x1) = {x2|(Ex3.(Ex4.x3 E x1
      & ~x4 E x3 & x2 = *union(x3,*sing(x4))))}

*nat = {x1|(Ax2.#ind(x2) -> x1 E x2)}

*nattwo = {x1|(Ax2.*one E x2
      & (Ax3.x3 E x2 -> *s(x3) E x2)
      -> x1 E x2)}

*natthree = {x1|(Ax2.x1 E x2 <- *one E x2
      & (Ax3.x3 E x2 -> *s(x3) E x2))}

*image(x1,x2) = {x3|<x2,x3> E x1}

*imageb(x1,x2) = {x3|(Ex4.x4 E x2 & <x4,x3> E x1)}

*converse(x1) = {x2|<p2(x2),p1(x2)> E x1}

*setdiff(x1,x2) = {x3|x3 E x1 & ~x3 E x2}

*u = {x1|x1 = x1}

*empty = {x1|~x1 = x1}

*comp(x1,x2) = {x3|(Ex4.<p1(x3),x4> E x2 & <x4,p2(x3)> E x1)}

*addfun(x1) = {x2|(Ax3.<*one,*s(x1)> E x3
      & (Ax4.(Ax5.<x4,x5> E x3
      -> <*s(x4),*s(x5)> E x3))
      -> x2 E x3)}

*theset(x1) = {x2|(Ex3.x1 = *sing(x3) & x2 E x3)}

*apply(x1,x2) = *theset({x3|<x2,x3> E x1})

*add(x1,x2) = *apply(*addfun(x1),x2)


Predicate definitions:


#neq(x1,x2) == ~x1 = x2

#ind(x1) == *one E x1
      & (Ax2.x2 E x1 -> *s(x2) E x1)

#relation(x1,x2,x3) == (Ax4.x4 E x3
      -> p1(x4) E x1 & p2(x4) E x2)

#function(x1,x2,x3) == 
     (#relation(x1,x2,x3)
      & (Ax4.x4 E x1 -> (Ex5.<x4,x5> E x3))) & (Ax4.(Ax5.
     x4 E x3
      & x5 E x3 & p1(x4) = p1(x5)
      -> p2(x4) = p2(x5)))

#samesize(x1,x2) == (Ex3.#function(x1,x2,x3)
      & #function(x2,x1,*converse(x3)))

#set(x1) == x1 = {x2|x2 E x1}

#injective(x1) == (Ax4.(Ax5.x4 E x1
      & x5 E x1 & p1(x4) = p1(x5)
      -> p2(x4) = p2(x5)))

#surjective(x1,x2) == (Ax4.x4 E x2 -> (Ex5.<x5,x4> E x1))

#addind(x1,x2) == x1 E *nat
      & #function(*nat,*nat,x2)
      & <*one,*s(x1)> E x2
      & (Ax3.(Ax4.
     <x3,x4> E x2 -> <*s(x3),*s(x4)> E x2))

#sets(x1) == #set(x1)
      & (Ax2.x2 E x1 -> #set(x2))

Line 3:  
----------Proved---------
1:  a1 E *nat
2:  a2 E a1


|-

1:  (Ax1.x1 E a1 == #samesize(x1,a2))


 by 4

Line 4:  
----------Proved---------
1:  (Ax8.#ind(x8) -> a1 E x8)
2:  a2 E a1


|-

1:  (Ax1.x1 E a1 == #samesize(x1,a2))


 by 5

Line 5:  
----------Proved---------
1:  
     #ind({x1|(Ax2.x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))})
      -> a1 E {x1|(Ax2.
     x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))}
2:  a2 E a1


|-

1:  (Ax1.x1 E a1 == #samesize(x1,a2))


 by 7, 6

Line 7:  
----------Proved---------
1:  a1 E {x1|(Ax2.x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))}
2:  a2 E a1


|-

1:  (Ax1.x1 E a1 == #samesize(x1,a2))


 by 1024

Line 1024:  
----------Proved---------
1:  (Ax4.x4 E a1
      -> (Ax6.x6 E a1 == #samesize(x6,x4)))
2:  a2 E a1


|-

1:  (Ax1.x1 E a1 == #samesize(x1,a2))


 by 1025

Line 1025:  
----------Proved---------
1:  a2 E a1
      -> (Ax7.x7 E a1 == #samesize(x7,a2))
2:  a2 E a1


|-

1:  (Ax1.x1 E a1 == #samesize(x1,a2))


 by MP


Proof of lemma MP starts:


Line MP.3:  
----------Proved---------
1:  P1 -> P2
2:  P1


|-

1:  P2


 by MP.5, 4

Line MP.5:  
----------Proved---------
1:  P2
2:  P1


|-

1:  P2




Line MP.4:  
----------Proved---------
1:  P1


|-

1:  P1
2:  P2





Proof of lemma MP ends


Line 6:  
----------Proved---------


|-

1:  #ind({x1|(Ax2.x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))})


 by 8

Line 8:  
----------Proved---------


|-

1:  
     *one E {x1|(Ax2.x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))}
      & (Ax5.
     x5 E {x1|(Ax2.
     x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))}
      -> *s(x5) E {x1|(Ax2.
     x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))})


 by 10, 9

Line 10:  
----------Proved---------


|-

1:  (Ax5.
     x5 E {x1|(Ax2.x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))}
      -> *s(x5) E {x1|(Ax2.
     x2 E x1
      -> (Ax3.x3 E x1 == #samesize(x3,x2)))})


 by 207

Line 207:  
----------Proved---------


|-

1:  
     a17 E {x4|(Ax8.x8 E x4
      -> (Ax10.x10 E x4 == #samesize(x10,x8)))}
      -> *s(a17) E {x11|(Ax15.
     x15 E x11
      -> (Ax17.x17 E x11 == #samesize(x17,x15)))}


 by 208

Line 208:  
----------Proved---------
1:  a17 E {x4|(Ax8.x8 E x4
      -> (Ax10.x10 E x4 == #samesize(x10,x8)))}


|-

1:  *s(a17) E {x11|(Ax15.x15 E x11
      -> (Ax17.x17 E x11 == #samesize(x17,x15)))}


 by 209

Line 209:  
----------Proved---------
1:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  *s(a17) E {x11|(Ax15.x15 E x11
      -> (Ax17.x17 E x11 == #samesize(x17,x15)))}


 by 210

Line 210:  
----------Proved---------
1:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  (Ax21.x21 E *s(a17)
      -> (Ax23.x23 E *s(a17) == #samesize(x23,x21)))


 by 211

Line 211:  
----------Proved---------
1:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  a18 E *s(a17)
      -> (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 212

Line 212:  
----------Proved---------
1:  a18 E *s(a17)
2:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 213

Line 213:  
----------Proved---------
1:  (Ex25.(Ex27.x25 E a17
      & ~x27 E x25 & a18 = *union(x25,*sing(x27))))
2:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 214

Line 214:  
----------Proved---------
1:  (Ex28.a19 E a17
      & ~x28 E a19 & a18 = *union(a19,*sing(x28)))
2:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 215

Line 215:  
----------Proved---------
1:  a19 E a17
      & ~a20 E a19 & a18 = *union(a19,*sing(a20))
2:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 216

Line 216:  
----------Proved---------
1:  ~a20 E a19 & a18 = *union(a19,*sing(a20))
2:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))
3:  a19 E a17


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 217

Line 217:  
----------Proved---------
1:  (Ax18.x18 E a17
      -> (Ax20.x20 E a17 == #samesize(x20,x18)))
2:  a19 E a17
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 218

Line 218:  
----------Proved---------
1:  a19 E a17
      -> (Ax29.x29 E a17 == #samesize(x29,a19))
2:  a19 E a17
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 220, 219

Line 220:  
----------Proved---------
1:  (Ax29.x29 E a17 == #samesize(x29,a19))
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))


|-

1:  (Ax24.x24 E *s(a17) == #samesize(x24,a18))


 by 221

Line 221:  
----------Proved---------
1:  (Ax29.x29 E a17 == #samesize(x29,a19))
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))


|-

1:  a21 E *s(a17) == #samesize(a21,a18)


 by 222

Line 222:  
----------Proved---------
1:  (Ax29.x29 E a17 == #samesize(x29,a19))
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))


|-

1:  
     (a21 E *s(a17) -> #samesize(a21,a18)) & (
     #samesize(a21,a18) -> a21 E *s(a17))


 by 224, 223

Line 224:  
----------Proved---------
1:  (Ax29.x29 E a17 == #samesize(x29,a19))
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))


|-

1:  #samesize(a21,a18) -> a21 E *s(a17)


 by 543

Line 543:  
----------Proved---------
1:  #samesize(a21,a18)
2:  (Ax29.x29 E a17 == #samesize(x29,a19))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))


|-

1:  a21 E *s(a17)


 by 544

Line 544:  
----------Proved---------
1:  (Ex4.#function(a21,a18,x4)
      & #function(a18,a21,*converse(x4)))
2:  (Ax29.x29 E a17 == #samesize(x29,a19))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))


|-

1:  a21 E *s(a17)


 by 545

Line 545:  
----------Proved---------
1:  #function(a21,a18,a36)
      & #function(a18,a21,*converse(a36))
2:  (Ax29.x29 E a17 == #samesize(x29,a19))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))


|-

1:  a21 E *s(a17)


 by 546

Line 546:  
----------Proved---------
1:  #function(a21,a18,a36)
      & #function(a18,a21,*converse(a36))
2:  (Ax29.x29 E a17 == #samesize(x29,a19))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 547

Line 547:  
----------Proved---------
1:  #function(a18,a21,*converse(a36))
2:  (Ax29.x29 E a17 == #samesize(x29,a19))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))
5:  #function(a21,a18,a36)


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 548

Line 548:  
----------Proved---------
1:  
     (#relation(a18,a21,*converse(a36))
      & (Ax6.x6 E a18
      -> (Ex10.<x6,x10> E *converse(a36)))) & (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))
2:  (Ax29.x29 E a17 == #samesize(x29,a19))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))
5:  #function(a21,a18,a36)


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 549

Line 549:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
      & (Ax6.x6 E a18
      -> (Ex10.<x6,x10> E *converse(a36)))
2:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
3:  (Ax29.x29 E a17 == #samesize(x29,a19))
4:  ~a20 E a19
5:  a18 = *union(a19,*sing(a20))
6:  #function(a21,a18,a36)


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 550

Line 550:  
----------Proved---------
1:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
2:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
3:  (Ax29.x29 E a17 == #samesize(x29,a19))
4:  ~a20 E a19
5:  a18 = *union(a19,*sing(a20))
6:  #function(a21,a18,a36)
7:  #relation(a18,a21,*converse(a36))


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 551

Line 551:  
----------Proved---------
1:  a20 E a18 -> (Ex22.<a20,x22> E *converse(a36))
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  (Ax29.x29 E a17 == #samesize(x29,a19))
5:  ~a20 E a19
6:  a18 = *union(a19,*sing(a20))
7:  #function(a21,a18,a36)
8:  #relation(a18,a21,*converse(a36))


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 553, 552

Line 553:  
----------Proved---------
1:  (Ex22.<a20,x22> E *converse(a36))
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  (Ax29.x29 E a17 == #samesize(x29,a19))
5:  ~a20 E a19
6:  a18 = *union(a19,*sing(a20))
7:  #function(a21,a18,a36)
8:  #relation(a18,a21,*converse(a36))


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 565

Line 565:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  (Ax29.x29 E a17 == #samesize(x29,a19))
5:  ~a20 E a19
6:  a18 = *union(a19,*sing(a20))
7:  #function(a21,a18,a36)
8:  #relation(a18,a21,*converse(a36))


|-

1:  (Ex19.(Ex21.x19 E a17
      & ~x21 E x19 & a21 = *union(x19,*sing(x21))))


 by 566

Line 566:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  (Ax29.x29 E a17 == #samesize(x29,a19))
5:  ~a20 E a19
6:  a18 = *union(a19,*sing(a20))
7:  #function(a21,a18,a36)
8:  #relation(a18,a21,*converse(a36))


|-

1:  (Ex22.*imageb(*converse(a36),a19) E a17
      & 
     ~x22 E *imageb(*converse(a36),a19)
      & a21 = *union(*imageb(*converse(a36),a19),*sing(x22)))


 by 567

Line 567:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  (Ax29.x29 E a17 == #samesize(x29,a19))
5:  ~a20 E a19
6:  a18 = *union(a19,*sing(a20))
7:  #function(a21,a18,a36)
8:  #relation(a18,a21,*converse(a36))


|-

1:  *imageb(*converse(a36),a19) E a17
      & 
     ~a37 E *imageb(*converse(a36),a19)
      & a21 = *union(*imageb(*converse(a36),a19),*sing(a37))


 by 569, 568

Line 569:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
3:  ~a20 E a19
4:  a18 = *union(a19,*sing(a20))
5:  #function(a21,a18,a36)
6:  #relation(a18,a21,*converse(a36))


|-

1:  ~a37 E *imageb(*converse(a36),a19)
      & a21 = *union(*imageb(*converse(a36),a19),*sing(a37))


 by 1023, 1022

Line 1023:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2


Proof of lemma Repeated2 starts:


Line Repeated2.678:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2.877

Line Repeated2.877:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  
     (Ex1.x1 E a21
      v x1 E *union(*imageb(*converse(a36),a19),*sing(a37)))
      & (Ax1.
     x1 E a21
      == x1 E *union(*imageb(*converse(a36),a19),*sing(a37)))


 by Repeated2.879, 878

Line Repeated2.879:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  (Ax1.x1 E a21
      == x1 E *union(*imageb(*converse(a36),a19),*sing(a37)))


 by Repeated2.885

Line Repeated2.885:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a59 E a21
      == a59 E *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2.886

Line Repeated2.886:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  
     (a59 E a21
      -> a59 E *union(*imageb(*converse(a36),a19),*sing(a37))) & (
     a59 E *union(*imageb(*converse(a36),a19),*sing(a37))
      -> a59 E a21)


 by Repeated2.888, 887

Line Repeated2.888:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
2:  <a20,a37> E *converse(a36)


|-

1:  
     a59 E *union(*imageb(*converse(a36),a19),*sing(a37))
      -> a59 E a21


 by Repeated2.931

Line Repeated2.931:  
----------Proved---------
1:  a59 E *union(*imageb(*converse(a36),a19),*sing(a37))
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.932

Line Repeated2.932:  
----------Proved---------
1:  a59 E *imageb(*converse(a36),a19)
      v a59 E *sing(a37)
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.934, 933

Line Repeated2.934:  
----------Proved---------
1:  a59 E *sing(a37)
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.943

Line Repeated2.943:  
----------Proved---------
1:  a59 = a37
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.944

Line Repeated2.944:  
----------Proved---------
1:  (Ax1.a59 E x1 == a37 E x1)
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.945

Line Repeated2.945:  
----------Proved---------
1:  a59 E a21 == a37 E a21
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.946

Line Repeated2.946:  
----------Proved---------
1:  (a59 E a21 -> a37 E a21) & (
     a37 E a21 -> a59 E a21)
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.947

Line Repeated2.947:  
----------Proved---------
1:  a37 E a21 -> a59 E a21
2:  #relation(a18,a21,*converse(a36))
3:  <a20,a37> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.949, 948

Line Repeated2.949:  
----------Proved---------
1:  a59 E a21


|-

1:  a59 E a21




Line Repeated2.948:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
2:  <a20,a37> E *converse(a36)


|-

1:  a37 E a21


 by Repeated2.950

Line Repeated2.950:  
----------Proved---------
1:  (Ax5.x5 E *converse(a36)
      -> p1(x5) E a18 & p2(x5) E a21)
2:  <a20,a37> E *converse(a36)


|-

1:  a37 E a21


 by Repeated2.951

Line Repeated2.951:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
      -> a20 E a18 & a37 E a21
2:  <a20,a37> E *converse(a36)


|-

1:  a37 E a21


 by Repeated2.953, 952

Line Repeated2.953:  
----------Proved---------
1:  a20 E a18 & a37 E a21


|-

1:  a37 E a21


 by Repeated2.954

Line Repeated2.954:  
----------Proved---------
1:  a37 E a21


|-

1:  a37 E a21




Line Repeated2.952:  
----------Proved---------
1:  <a20,a37> E *converse(a36)


|-

1:  <a20,a37> E *converse(a36)




Line Repeated2.933:  
----------Proved---------
1:  a59 E *imageb(*converse(a36),a19)
2:  #relation(a18,a21,*converse(a36))


|-

1:  a59 E a21


 by Repeated2.935

Line Repeated2.935:  
----------Proved---------
1:  (Ex18.x18 E a19 & <x18,a59> E *converse(a36))
2:  #relation(a18,a21,*converse(a36))


|-

1:  a59 E a21


 by Repeated2.936

Line Repeated2.936:  
----------Proved---------
1:  a61 E a19 & <a61,a59> E *converse(a36)
2:  #relation(a18,a21,*converse(a36))


|-

1:  a59 E a21


 by Repeated2.937

Line Repeated2.937:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
2:  <a61,a59> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.938

Line Repeated2.938:  
----------Proved---------
1:  (Ax5.x5 E *converse(a36)
      -> p1(x5) E a18 & p2(x5) E a21)
2:  <a61,a59> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.939

Line Repeated2.939:  
----------Proved---------
1:  <a61,a59> E *converse(a36)
      -> a61 E a18 & a59 E a21
2:  <a61,a59> E *converse(a36)


|-

1:  a59 E a21


 by Repeated2.941, 940

Line Repeated2.941:  
----------Proved---------
1:  a61 E a18 & a59 E a21


|-

1:  a59 E a21


 by Repeated2.942

Line Repeated2.942:  
----------Proved---------
1:  a59 E a21


|-

1:  a59 E a21




Line Repeated2.940:  
----------Proved---------
1:  <a61,a59> E *converse(a36)


|-

1:  <a61,a59> E *converse(a36)




Line Repeated2.887:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a59 E a21
      -> a59 E *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2.889

Line Repeated2.889:  
----------Proved---------
1:  a59 E a21
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a59 E *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2.890

Line Repeated2.890:  
----------Proved---------
1:  a59 E a21
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a59 E *imageb(*converse(a36),a19)
      v a59 E *sing(a37)


 by Repeated2.891

Line Repeated2.891:  
----------Proved---------
1:  a59 E a21
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a59 E *imageb(*converse(a36),a19)
2:  a59 E *sing(a37)


 by Repeated2.892

Line Repeated2.892:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a59 E a21
5:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.893

Line Repeated2.893:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a59 E a21
5:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.894

Line Repeated2.894:  
----------Proved---------
1:  #relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36))
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a59 E a21
5:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.895

Line Repeated2.895:  
----------Proved---------
1:  (Ax6.x6 E a21 -> (Ex10.<x6,x10> E a36))
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a59 E a21
5:  a18 = *union(a19,*sing(a20))
6:  #relation(a21,a18,a36)


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.896

Line Repeated2.896:  
----------Proved---------
1:  a59 E a21 -> (Ex11.<a59,x11> E a36)
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a59 E a21
5:  a18 = *union(a19,*sing(a20))
6:  #relation(a21,a18,a36)


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.898, 897

Line Repeated2.898:  
----------Proved---------
1:  (Ex11.<a59,x11> E a36)
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a18 = *union(a19,*sing(a20))
5:  #relation(a21,a18,a36)


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.899

Line Repeated2.899:  
----------Proved---------
1:  <a59,a60> E a36
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a18 = *union(a19,*sing(a20))
5:  #relation(a21,a18,a36)


|-

1:  (Ex10.x10 E a19 & <x10,a59> E *converse(a36))
2:  a59 E *sing(a37)


 by Repeated2.900

Line Repeated2.900:  
----------Proved---------
1:  <a59,a60> E a36
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a18 = *union(a19,*sing(a20))
5:  #relation(a21,a18,a36)


|-

1:  a60 E a19 & <a60,a59> E *converse(a36)
2:  a59 E *sing(a37)


 by Repeated2.902, 901

Line Repeated2.902:  
----------Proved---------
1:  <a59,a60> E a36


|-

1:  <a60,a59> E *converse(a36)


 by Repeated2.930

Line Repeated2.930:  
----------Proved---------
1:  <a59,a60> E a36


|-

1:  <a59,a60> E a36




Line Repeated2.901:  
----------Proved---------
1:  #relation(a21,a18,a36)
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a18 = *union(a19,*sing(a20))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.903

Line Repeated2.903:  
----------Proved---------
1:  (Ax5.x5 E a36
      -> p1(x5) E a21 & p2(x5) E a18)
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a18 = *union(a19,*sing(a20))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.904

Line Repeated2.904:  
----------Proved---------
1:  <a59,a60> E a36
      -> a59 E a21 & a60 E a18
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a18 = *union(a19,*sing(a20))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.906, 905

Line Repeated2.906:  
----------Proved---------
1:  a59 E a21 & a60 E a18
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a18 = *union(a19,*sing(a20))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.907

Line Repeated2.907:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  a60 E a18
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.908

Line Repeated2.908:  
----------Proved---------
1:  (Ax1.a18 E x1 == *union(a19,*sing(a20)) E x1)
2:  a60 E a18
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.909

Line Repeated2.909:  
----------Proved---------
1:  a18 E {x1|a60 E x1}
      == *union(a19,*sing(a20)) E {x1|a60 E x1}
2:  a60 E a18
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.910

Line Repeated2.910:  
----------Proved---------
1:  
     (a18 E {x1|a60 E x1}
      -> *union(a19,*sing(a20)) E {x1|a60 E x1}) & (
     *union(a19,*sing(a20)) E {x1|a60 E x1}
      -> a18 E {x1|a60 E x1})
2:  a60 E a18
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.911

Line Repeated2.911:  
----------Proved---------
1:  a18 E {x1|a60 E x1}
      -> *union(a19,*sing(a20)) E {x1|a60 E x1}
2:  a60 E a18
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.913, 912

Line Repeated2.913:  
----------Proved---------
1:  *union(a19,*sing(a20)) E {x1|a60 E x1}
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.915

Line Repeated2.915:  
----------Proved---------
1:  a60 E *union(a19,*sing(a20))
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.916

Line Repeated2.916:  
----------Proved---------
1:  a60 E a19 v a60 E *sing(a20)
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a60 E a19
2:  a59 E *sing(a37)


 by Repeated2.918, 917

Line Repeated2.918:  
----------Proved---------
1:  a60 E *sing(a20)
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a59 E *sing(a37)


 by Repeated2.919

Line Repeated2.919:  
----------Proved---------
1:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a60 = a20
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)


|-

1:  a59 E *sing(a37)


 by Repeated2.920

Line Repeated2.920:  
----------Proved---------
1:  (Ax17.
     <a60,a59> E *converse(a36) & x17 E *converse(a36)
      & a60 = p1(x17) -> a59 = p2(x17))
2:  a60 = a20
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)


|-

1:  a59 E *sing(a37)


 by Repeated2.921

Line Repeated2.921:  
----------Proved---------
1:  
     <a60,a59> E *converse(a36) & 
     <a20,a37> E *converse(a36) & a60 = a20
      -> a59 = a37
2:  a60 = a20
3:  <a59,a60> E a36
4:  <a20,a37> E *converse(a36)


|-

1:  a59 E *sing(a37)


 by Repeated2.923, 922

Line Repeated2.923:  
----------Proved---------
1:  a59 = a37


|-

1:  a59 E *sing(a37)


 by Repeated2.929

Line Repeated2.929:  
----------Proved---------
1:  a59 = a37


|-

1:  a59 = a37




Line Repeated2.922:  
----------Proved---------
1:  a60 = a20
2:  <a59,a60> E a36
3:  <a20,a37> E *converse(a36)


|-

1:  <a60,a59> E *converse(a36) & 
     <a20,a37> E *converse(a36) & a60 = a20


 by Repeated2.925, 924

Line Repeated2.925:  
----------Proved---------
1:  a60 = a20
2:  <a20,a37> E *converse(a36)


|-

1:  <a20,a37> E *converse(a36) & a60 = a20


 by Repeated2.928, 927

Line Repeated2.928:  
----------Proved---------
1:  a60 = a20


|-

1:  a60 = a20




Line Repeated2.927:  
----------Proved---------
1:  <a20,a37> E *converse(a36)


|-

1:  <a20,a37> E *converse(a36)




Line Repeated2.924:  
----------Proved---------
1:  <a59,a60> E a36


|-

1:  <a60,a59> E *converse(a36)


 by Repeated2.926

Line Repeated2.926:  
----------Proved---------
1:  <a59,a60> E a36


|-

1:  <a59,a60> E a36




Line Repeated2.917:  
----------Proved---------
1:  a60 E a19


|-

1:  a60 E a19




Line Repeated2.912:  
----------Proved---------
1:  a60 E a18


|-

1:  a18 E {x1|a60 E x1}


 by Repeated2.914

Line Repeated2.914:  
----------Proved---------
1:  a60 E a18


|-

1:  a60 E a18




Line Repeated2.905:  
----------Proved---------
1:  <a59,a60> E a36


|-

1:  <a59,a60> E a36




Line Repeated2.897:  
----------Proved---------
1:  a59 E a21


|-

1:  a59 E a21




Line Repeated2.878:  
----------Proved---------


|-

1:  (Ex1.x1 E a21
      v x1 E *union(*imageb(*converse(a36),a19),*sing(a37)))


 by Repeated2.880

Line Repeated2.880:  
----------Proved---------


|-

1:  a37 E a21
      v a37 E *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2.881

Line Repeated2.881:  
----------Proved---------


|-

1:  a37 E *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2.882

Line Repeated2.882:  
----------Proved---------


|-

1:  a37 E *imageb(*converse(a36),a19)
      v a37 E *sing(a37)


 by Repeated2.883

Line Repeated2.883:  
----------Proved---------


|-

1:  a37 E *sing(a37)


 by Repeated2.884

Line Repeated2.884:  
----------Proved---------


|-

1:  a37 = a37


 by Repeated2.REFLEQ


Proof of lemma Repeated2.REFLEQ starts:


Line Repeated2.REFLEQ.1:  
----------Proved---------


|-

1:  x1 = x1


 by Repeated2.REFLEQ.2

Line Repeated2.REFLEQ.2:  
----------Proved---------


|-

1:  (Ax2.x1 E x2 == x1 E x2)
2:  (Ex2.x2 E x1 v x2 E x1) & (Ax2.x2 E x1
      == x2 E x1)


 by Repeated2.REFLEQ.3

Line Repeated2.REFLEQ.3:  
----------Proved---------


|-

1:  x1 E a1 == x1 E a1


 by Repeated2.REFLEQ.Triv2


Proof of lemma Repeated2.REFLEQ.Triv2 starts:


Line Repeated2.REFLEQ.Triv2.1:  
----------Proved---------


|-

1:  P1 == P1


 by Repeated2.REFLEQ.Triv2.2

Line Repeated2.REFLEQ.Triv2.2:  
----------Proved---------


|-

1:  (P1 -> P1) & (P1 -> P1)


 by Repeated2.REFLEQ.Triv2.4, 3

Line Repeated2.REFLEQ.Triv2.4:  
----------Proved---------


|-

1:  P1 -> P1


 by Repeated2.REFLEQ.Triv2.Triv1


Proof of lemma Repeated2.REFLEQ.Triv2.Triv1 starts:


Line Repeated2.REFLEQ.Triv2.Triv1.1:  
----------Proved---------


|-

1:  P1 -> P1


 by Repeated2.REFLEQ.Triv2.Triv1.2

Line Repeated2.REFLEQ.Triv2.Triv1.2:  
----------Proved---------
1:  P1


|-

1:  P1





Proof of lemma Repeated2.REFLEQ.Triv2.Triv1 ends


Line Repeated2.REFLEQ.Triv2.3:  
----------Proved---------


|-

1:  P1 -> P1


 by Repeated2.REFLEQ.Triv2.Triv1


Proof of lemma Repeated2.REFLEQ.Triv2 ends



Proof of lemma Repeated2.REFLEQ ends



Proof of lemma Repeated2 ends


Line 1022:  
----------Proved---------
1:  ~a20 E a19
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)


|-

1:  ~a37 E *imageb(*converse(a36),a19)


 by Repeated1


Proof of lemma Repeated1 starts:


Line Repeated1.676:  
----------Proved---------
1:  ~a20 E a19
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)


|-

1:  ~a37 E *imageb(*converse(a36),a19)


 by Repeated1.955

Line Repeated1.955:  
----------Proved---------
1:  a37 E *imageb(*converse(a36),a19)
2:  ~a20 E a19
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)


|-



 by Repeated1.956

Line Repeated1.956:  
----------Proved---------
1:  (Ex10.x10 E a19 & <x10,a37> E *converse(a36))
2:  ~a20 E a19
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)


|-



 by Repeated1.957

Line Repeated1.957:  
----------Proved---------
1:  a62 E a19 & <a62,a37> E *converse(a36)
2:  ~a20 E a19
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)


|-



 by Repeated1.958

Line Repeated1.958:  
----------Proved---------
1:  <a62,a37> E *converse(a36)
2:  ~a20 E a19
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  a62 E a19


|-



 by Repeated1.959

Line Repeated1.959:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  a62 E a19
3:  <a37,a62> E a36
4:  ~a20 E a19
5:  #function(a21,a18,a36)


|-



 by Repeated1.960

Line Repeated1.960:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  <a37,a20> E a36
3:  a62 E a19
4:  <a37,a62> E a36
5:  ~a20 E a19


|-



 by Repeated1.961

Line Repeated1.961:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  <a37,a20> E a36
3:  a62 E a19
4:  <a37,a62> E a36
5:  ~a20 E a19


|-



 by Repeated1.962

Line Repeated1.962:  
----------Proved---------
1:  (Ax12.(Ax16.x12 E a36
      & x16 E a36 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))
2:  <a37,a20> E a36
3:  a62 E a19
4:  <a37,a62> E a36
5:  ~a20 E a19


|-



 by Repeated1.963

Line Repeated1.963:  
----------Proved---------
1:  (Ax17.<a37,a20> E a36
      & x17 E a36 & a37 = p1(x17)
      -> a20 = p2(x17))
2:  <a37,a20> E a36
3:  a62 E a19
4:  <a37,a62> E a36
5:  ~a20 E a19


|-



 by Repeated1.964

Line Repeated1.964:  
----------Proved---------
1:  <a37,a20> E a36
      & <a37,a62> E a36 & a37 = a37
      -> a20 = a62
2:  <a37,a20> E a36
3:  a62 E a19
4:  <a37,a62> E a36
5:  ~a20 E a19


|-



 by Repeated1.966, 965

Line Repeated1.966:  
----------Proved---------
1:  a20 = a62
2:  a62 E a19
3:  ~a20 E a19


|-



 by Repeated1.971

Line Repeated1.971:  
----------Proved---------
1:  (Ax1.a20 E x1 == a62 E x1)
2:  a62 E a19
3:  ~a20 E a19


|-



 by Repeated1.972

Line Repeated1.972:  
----------Proved---------
1:  a20 E a19 == a62 E a19
2:  a62 E a19
3:  ~a20 E a19


|-



 by Repeated1.973

Line Repeated1.973:  
----------Proved---------
1:  (a20 E a19 -> a62 E a19) & (
     a62 E a19 -> a20 E a19)
2:  a62 E a19
3:  ~a20 E a19


|-



 by Repeated1.974

Line Repeated1.974:  
----------Proved---------
1:  a62 E a19 -> a20 E a19
2:  a62 E a19
3:  ~a20 E a19


|-



 by Repeated1.976, 975

Line Repeated1.976:  
----------Proved---------
1:  ~a20 E a19
2:  a20 E a19


|-



 by Repeated1.977

Line Repeated1.977:  
----------Proved---------
1:  a20 E a19


|-

1:  a20 E a19




Line Repeated1.975:  
----------Proved---------
1:  a62 E a19


|-

1:  a62 E a19




Line Repeated1.965:  
----------Proved---------
1:  <a37,a20> E a36
2:  <a37,a62> E a36


|-

1:  <a37,a20> E a36
      & <a37,a62> E a36 & a37 = a37


 by Repeated1.968, 967

Line Repeated1.968:  
----------Proved---------
1:  <a37,a62> E a36


|-

1:  <a37,a62> E a36 & a37 = a37


 by Repeated1.970, 969

Line Repeated1.970:  
----------Proved---------


|-

1:  a37 = a37


 by Repeated1.REFLEQ


Proof of lemma Repeated1.REFLEQ starts:


Line Repeated1.REFLEQ.1:  
----------Proved---------


|-

1:  x1 = x1


 by Repeated1.REFLEQ.2

Line Repeated1.REFLEQ.2:  
----------Proved---------


|-

1:  (Ax2.x1 E x2 == x1 E x2)
2:  (Ex2.x2 E x1 v x2 E x1) & (Ax2.x2 E x1
      == x2 E x1)


 by Repeated1.REFLEQ.3

Line Repeated1.REFLEQ.3:  
----------Proved---------


|-

1:  x1 E a1 == x1 E a1


 by Repeated1.REFLEQ.Triv2


Proof of lemma Repeated1.REFLEQ.Triv2 starts:


Line Repeated1.REFLEQ.Triv2.1:  
----------Proved---------


|-

1:  P1 == P1


 by Repeated1.REFLEQ.Triv2.2

Line Repeated1.REFLEQ.Triv2.2:  
----------Proved---------


|-

1:  (P1 -> P1) & (P1 -> P1)


 by Repeated1.REFLEQ.Triv2.4, 3

Line Repeated1.REFLEQ.Triv2.4:  
----------Proved---------


|-

1:  P1 -> P1


 by Repeated1.REFLEQ.Triv2.Triv1


Proof of lemma Repeated1.REFLEQ.Triv2.Triv1 starts:


Line Repeated1.REFLEQ.Triv2.Triv1.1:  
----------Proved---------


|-

1:  P1 -> P1


 by Repeated1.REFLEQ.Triv2.Triv1.2

Line Repeated1.REFLEQ.Triv2.Triv1.2:  
----------Proved---------
1:  P1


|-

1:  P1





Proof of lemma Repeated1.REFLEQ.Triv2.Triv1 ends


Line Repeated1.REFLEQ.Triv2.3:  
----------Proved---------


|-

1:  P1 -> P1


 by Repeated1.REFLEQ.Triv2.Triv1


Proof of lemma Repeated1.REFLEQ.Triv2 ends



Proof of lemma Repeated1.REFLEQ ends


Line Repeated1.969:  
----------Proved---------
1:  <a37,a62> E a36


|-

1:  <a37,a62> E a36




Line Repeated1.967:  
----------Proved---------
1:  <a37,a20> E a36


|-

1:  <a37,a20> E a36





Proof of lemma Repeated1 ends


Line 568:  
----------Proved---------
1:  (Ax29.x29 E a17 == #samesize(x29,a19))
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))
4:  #function(a21,a18,a36)
5:  #relation(a18,a21,*converse(a36))
6:  <a20,a37> E *converse(a36)
7:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
8:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  *imageb(*converse(a36),a19) E a17


 by 570

Line 570:  
----------Proved---------
1:  *imageb(*converse(a36),a19) E a17
      == #samesize(*imageb(*converse(a36),a19),a19)
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))
4:  #function(a21,a18,a36)
5:  #relation(a18,a21,*converse(a36))
6:  <a20,a37> E *converse(a36)
7:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
8:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  *imageb(*converse(a36),a19) E a17


 by 571

Line 571:  
----------Proved---------
1:  
     (*imageb(*converse(a36),a19) E a17
      -> #samesize(*imageb(*converse(a36),a19),a19)) & (
     #samesize(*imageb(*converse(a36),a19),a19)
      -> *imageb(*converse(a36),a19) E a17)
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))
4:  #function(a21,a18,a36)
5:  #relation(a18,a21,*converse(a36))
6:  <a20,a37> E *converse(a36)
7:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
8:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  *imageb(*converse(a36),a19) E a17


 by 572

Line 572:  
----------Proved---------
1:  #samesize(*imageb(*converse(a36),a19),a19)
      -> *imageb(*converse(a36),a19) E a17
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))
4:  #function(a21,a18,a36)
5:  #relation(a18,a21,*converse(a36))
6:  <a20,a37> E *converse(a36)
7:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
8:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  *imageb(*converse(a36),a19) E a17


 by 574, 573

Line 574:  
----------Proved---------
1:  *imageb(*converse(a36),a19) E a17


|-

1:  *imageb(*converse(a36),a19) E a17




Line 573:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  #relation(a18,a21,*converse(a36))
5:  <a20,a37> E *converse(a36)
6:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
7:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #samesize(*imageb(*converse(a36),a19),a19)


 by 575

Line 575:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  #relation(a18,a21,*converse(a36))
5:  <a20,a37> E *converse(a36)
6:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
7:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  (Ex4.#function(*imageb(*converse(a36),a19),a19,x4)
      & #function(a19,*imageb(*converse(a36),a19),*converse(x4)))


 by 576

Line 576:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  #relation(a18,a21,*converse(a36))
5:  <a20,a37> E *converse(a36)
6:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
7:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  (Ex4.#function(*imageb(*converse(a36),a19),a19,x4)
      & #function(a19,*imageb(*converse(a36),a19),*converse(x4)))


 by 577

Line 577:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  #relation(a18,a21,*converse(a36))
5:  <a20,a37> E *converse(a36)
6:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
7:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  
     #function(*imageb(*converse(a36),a19),a19,*setdiff(a36,*sing(<a37,a20>)))
      & #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 579, 578

Line 579:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  #relation(a18,a21,*converse(a36))
5:  <a20,a37> E *converse(a36)
6:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
7:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 674, 673

Line 674:  
----------Proved---------


|-

1:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))


 by 978

Line 978:  
----------Proved---------


|-

1:  {x3|<p2(x3),p1(x3)> E *setdiff(a36,*sing(<a37,a20>))} = *setdiff(*converse(a36),*sing(<a20,a37>))


 by 979

Line 979:  
----------Proved---------


|-

1:  {x3|<p2(x3),p1(x3)> E *setdiff(a36,*sing(<a37,a20>))} = {x4|x4 E *converse(a36) & ~x4 E *sing(<a20,a37>)}


 by 980

Line 980:  
----------Proved---------


|-

1:  (Ax3.<p2(x3),p1(x3)> E *setdiff(a36,*sing(<a37,a20>))
      == 
     x3 E *converse(a36) & ~x3 E *sing(<a20,a37>))


 by 981

Line 981:  
----------Proved---------


|-

1:  <p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>)) == 
     a63 E *converse(a36)
      & ~a63 E *sing(<a20,a37>)


 by 982

Line 982:  
----------Proved---------


|-

1:  
     (<p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>)) -> 
     a63 E *converse(a36)
      & ~a63 E *sing(<a20,a37>))
      & (
     a63 E *converse(a36)
      & ~a63 E *sing(<a20,a37>)
      -> <p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>)))


 by 984, 983

Line 984:  
----------Proved---------


|-

1:  
     a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)
      -> <p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>))


 by 1003

Line 1003:  
----------Proved---------
1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


|-

1:  <p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>))


 by 1004

Line 1004:  
----------Proved---------
1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


|-

1:  <p2(a63),p1(a63)> E a36
      & ~<p2(a63),p1(a63)> E *sing(<a37,a20>)


 by 1006, 1005

Line 1006:  
----------Proved---------
1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


|-

1:  ~<p2(a63),p1(a63)> E *sing(<a37,a20>)


 by 1009

Line 1009:  
----------Proved---------
1:  <p2(a63),p1(a63)> E *sing(<a37,a20>)
2:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


|-



 by 1010

Line 1010:  
----------Proved---------
1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)
2:  <p2(a63),p1(a63)> = <a37,a20>


|-



 by 1011

Line 1011:  
----------Proved---------
1:  ~a63 E *sing(<a20,a37>)
2:  <p2(a63),p1(a63)> = <a37,a20>


|-



 by 1012

Line 1012:  
----------Proved---------
1:  <p2(a63),p1(a63)> = <a37,a20>


|-

1:  a63 E *sing(<a20,a37>)


 by 1013

Line 1013:  
----------Proved---------
1:  <p2(a63),p1(a63)> = <a37,a20>


|-

1:  a63 = <a20,a37>


 by 1014

Line 1014:  
----------Proved---------
1:  (Ax1.<p2(a63),p1(a63)> E x1 == <a37,a20> E x1)


|-

1:  a63 = <a20,a37>


 by 1015

Line 1015:  
----------Proved---------
1:  
     <p2(a63),p1(a63)> E {x1|<p2(x1),p1(x1)> = <a20,a37>}
      == <a37,a20> E {x1|<p2(x1),p1(x1)> = <a20,a37>}


|-

1:  a63 = <a20,a37>


 by 1016

Line 1016:  
----------Proved---------
1:  
     (
     <p2(a63),p1(a63)> E {x1|<p2(x1),p1(x1)> = <a20,a37>}
      -> <a37,a20> E {x1|<p2(x1),p1(x1)> = <a20,a37>})
      & (
     <a37,a20> E {x1|<p2(x1),p1(x1)> = <a20,a37>}
      -> <p2(a63),p1(a63)> E {x1|<p2(x1),p1(x1)> = <a20,a37>})


|-

1:  a63 = <a20,a37>


 by 1017

Line 1017:  
----------Proved---------
1:  <a37,a20> E {x1|<p2(x1),p1(x1)> = <a20,a37>}
      -> <p2(a63),p1(a63)> E {x1|<p2(x1),p1(x1)> = <a20,a37>}


|-

1:  a63 = <a20,a37>


 by 1019, 1018

Line 1019:  
----------Proved---------
1:  <p2(a63),p1(a63)> E {x1|<p2(x1),p1(x1)> = <a20,a37>}


|-

1:  a63 = <a20,a37>


 by 1021

Line 1021:  
----------Proved---------
1:  a63 = <a20,a37>


|-

1:  a63 = <a20,a37>




Line 1018:  
----------Proved---------


|-

1:  <a37,a20> E {x1|<p2(x1),p1(x1)> = <a20,a37>}


 by 1020

Line 1020:  
----------Proved---------


|-

1:  <a20,a37> = <a20,a37>


 by REFLEQ


Proof of lemma REFLEQ starts:


Line REFLEQ.1:  
----------Proved---------


|-

1:  x1 = x1


 by REFLEQ.2

Line REFLEQ.2:  
----------Proved---------


|-

1:  (Ax2.x1 E x2 == x1 E x2)
2:  (Ex2.x2 E x1 v x2 E x1) & (Ax2.x2 E x1
      == x2 E x1)


 by REFLEQ.3

Line REFLEQ.3:  
----------Proved---------


|-

1:  x1 E a1 == x1 E a1


 by REFLEQ.Triv2


Proof of lemma REFLEQ.Triv2 starts:


Line REFLEQ.Triv2.1:  
----------Proved---------


|-

1:  P1 == P1


 by REFLEQ.Triv2.2

Line REFLEQ.Triv2.2:  
----------Proved---------


|-

1:  (P1 -> P1) & (P1 -> P1)


 by REFLEQ.Triv2.4, 3

Line REFLEQ.Triv2.4:  
----------Proved---------


|-

1:  P1 -> P1


 by REFLEQ.Triv2.Triv1


Proof of lemma REFLEQ.Triv2.Triv1 starts:


Line REFLEQ.Triv2.Triv1.1:  
----------Proved---------


|-

1:  P1 -> P1


 by REFLEQ.Triv2.Triv1.2

Line REFLEQ.Triv2.Triv1.2:  
----------Proved---------
1:  P1


|-

1:  P1





Proof of lemma REFLEQ.Triv2.Triv1 ends


Line REFLEQ.Triv2.3:  
----------Proved---------


|-

1:  P1 -> P1


 by REFLEQ.Triv2.Triv1


Proof of lemma REFLEQ.Triv2 ends



Proof of lemma REFLEQ ends


Line 1005:  
----------Proved---------
1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


|-

1:  <p2(a63),p1(a63)> E a36


 by 1007

Line 1007:  
----------Proved---------
1:  a63 E *converse(a36)


|-

1:  <p2(a63),p1(a63)> E a36


 by 1008

Line 1008:  
----------Proved---------
1:  <p2(a63),p1(a63)> E a36


|-

1:  <p2(a63),p1(a63)> E a36




Line 983:  
----------Proved---------


|-

1:  <p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>)) -> 
     a63 E *converse(a36)
      & ~a63 E *sing(<a20,a37>)


 by 985

Line 985:  
----------Proved---------
1:  <p2(a63),p1(a63)> E *setdiff(a36,*sing(<a37,a20>))


|-

1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


 by 986

Line 986:  
----------Proved---------
1:  <p2(a63),p1(a63)> E a36
      & ~<p2(a63),p1(a63)> E *sing(<a37,a20>)


|-

1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


 by 987

Line 987:  
----------Proved---------
1:  ~<p2(a63),p1(a63)> E *sing(<a37,a20>)
2:  <p2(a63),p1(a63)> E a36


|-

1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


 by 988

Line 988:  
----------Proved---------
1:  <p2(a63),p1(a63)> E a36


|-

1:  <p2(a63),p1(a63)> E *sing(<a37,a20>)
2:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)


 by 989

Line 989:  
----------Proved---------
1:  <p2(a63),p1(a63)> E a36


|-

1:  a63 E *converse(a36) & ~a63 E *sing(<a20,a37>)
2:  <p2(a63),p1(a63)> = <a37,a20>


 by 991, 990

Line 991:  
----------Proved---------


|-

1:  ~a63 E *sing(<a20,a37>)
2:  <p2(a63),p1(a63)> = <a37,a20>


 by 993

Line 993:  
----------Proved---------
1:  a63 E *sing(<a20,a37>)


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 994

Line 994:  
----------Proved---------
1:  a63 = <a20,a37>


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 995

Line 995:  
----------Proved---------
1:  (Ax1.a63 E x1 == <a20,a37> E x1)


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 996

Line 996:  
----------Proved---------
1:  a63 E {x1|<p2(x1),p1(x1)> = <a37,a20>}
      == <a20,a37> E {x1|<p2(x1),p1(x1)> = <a37,a20>}


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 997

Line 997:  
----------Proved---------
1:  
     (a63 E {x1|<p2(x1),p1(x1)> = <a37,a20>}
      -> <a20,a37> E {x1|<p2(x1),p1(x1)> = <a37,a20>})
      & (
     <a20,a37> E {x1|<p2(x1),p1(x1)> = <a37,a20>}
      -> a63 E {x1|<p2(x1),p1(x1)> = <a37,a20>})


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 998

Line 998:  
----------Proved---------
1:  <a20,a37> E {x1|<p2(x1),p1(x1)> = <a37,a20>}
      -> a63 E {x1|<p2(x1),p1(x1)> = <a37,a20>}


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 1000, 999

Line 1000:  
----------Proved---------
1:  a63 E {x1|<p2(x1),p1(x1)> = <a37,a20>}


|-

1:  <p2(a63),p1(a63)> = <a37,a20>


 by 1002

Line 1002:  
----------Proved---------
1:  <p2(a63),p1(a63)> = <a37,a20>


|-

1:  <p2(a63),p1(a63)> = <a37,a20>




Line 999:  
----------Proved---------


|-

1:  <a20,a37> E {x1|<p2(x1),p1(x1)> = <a37,a20>}


 by 1001

Line 1001:  
----------Proved---------


|-

1:  <a37,a20> = <a37,a20>


 by REFLEQ

Line 990:  
----------Proved---------
1:  <p2(a63),p1(a63)> E a36


|-

1:  a63 E *converse(a36)


 by 992

Line 992:  
----------Proved---------
1:  <p2(a63),p1(a63)> E a36


|-

1:  <p2(a63),p1(a63)> E a36




Line 673:  
----------Proved---------
1:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))
2:  ~a20 E a19
3:  a18 = *union(a19,*sing(a20))
4:  #function(a21,a18,a36)
5:  #relation(a18,a21,*converse(a36))
6:  <a20,a37> E *converse(a36)
7:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
8:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 676, 675

Line 676:  
----------Proved---------
1:  ~a20 E a19
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)


|-

1:  ~a37 E *imageb(*converse(a36),a19)


 by Repeated1

Line 675:  
----------Proved---------
1:  ~a37 E *imageb(*converse(a36),a19)
2:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))
3:  a18 = *union(a19,*sing(a20))
4:  #function(a21,a18,a36)
5:  #relation(a18,a21,*converse(a36))
6:  <a20,a37> E *converse(a36)
7:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
8:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 678, 677

Line 678:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  #relation(a18,a21,*converse(a36))
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))


 by Repeated2

Line 677:  
----------Proved---------
1:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
2:  ~a37 E *imageb(*converse(a36),a19)
3:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))
4:  a18 = *union(a19,*sing(a20))
5:  #function(a21,a18,a36)
6:  #relation(a18,a21,*converse(a36))
7:  <a20,a37> E *converse(a36)
8:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
9:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 680, 679

Line 680:  
----------Proved---------
1:  <a20,a37> E *converse(a36)


|-

1:  <a37,a20> E *converse(*converse(a36))


 by 874

Line 874:  
----------Proved---------
1:  <a20,a37> E *converse(a36)


|-

1:  <a20,a37> E *converse(a36)


 by 875

Line 875:  
----------Proved---------
1:  <a20,a37> E *converse(a36)


|-

1:  <a37,a20> E a36


 by 876

Line 876:  
----------Proved---------
1:  <a37,a20> E a36


|-

1:  <a37,a20> E a36




Line 679:  
----------Proved---------
1:  <a37,a20> E *converse(*converse(a36))
2:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
3:  ~a37 E *imageb(*converse(a36),a19)
4:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))
5:  a18 = *union(a19,*sing(a20))
6:  #function(a21,a18,a36)
7:  #relation(a18,a21,*converse(a36))
8:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
9:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 682, 681

Line 682:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(a18,a21,*converse(a36))


 by 869

Line 869:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  
     (#relation(a18,a21,*converse(a36))
      & (Ax6.x6 E a18
      -> (Ex10.<x6,x10> E *converse(a36)))) & (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))


 by 871, 870

Line 871:  
----------Proved---------
1:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))




Line 870:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  #relation(a18,a21,*converse(a36))
      & (Ax6.x6 E a18
      -> (Ex10.<x6,x10> E *converse(a36)))


 by 873, 872

Line 873:  
----------Proved---------
1:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))




Line 872:  
----------Proved---------
1:  #relation(a18,a21,*converse(a36))


|-

1:  #relation(a18,a21,*converse(a36))




Line 681:  
----------Proved---------
1:  #function(a18,a21,*converse(a36))
2:  <a37,a20> E *converse(*converse(a36))
3:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
4:  ~a37 E *imageb(*converse(a36),a19)
5:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))
6:  a18 = *union(a19,*sing(a20))
7:  #function(a21,a18,a36)
8:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 684, 683

Line 684:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  #function(a21,a18,*converse(*converse(a36)))


 by 823

Line 823:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  
     (#relation(a21,a18,*converse(*converse(a36)))
      & (Ax6.
     x6 E a21
      -> (Ex10.<x6,x10> E *converse(*converse(a36))))) & (Ax12.(Ax16.
     x12 E *converse(*converse(a36)) & 
     x16 E *converse(*converse(a36))
      & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))


 by 825, 824

Line 825:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  (Ax12.(Ax16.
     x12 E *converse(*converse(a36)) & 
     x16 E *converse(*converse(a36))
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


 by 850

Line 850:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  (Ax23.
     a57 E *converse(*converse(a36)) & 
     x23 E *converse(*converse(a36))
      & p1(a57) = p1(x23) -> p2(a57) = p2(x23))


 by 851

Line 851:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  
     a57 E *converse(*converse(a36)) & 
     a58 E *converse(*converse(a36))
      & p1(a57) = p1(a58) -> p2(a57) = p2(a58)


 by 852

Line 852:  
----------Proved---------
1:  a57 E *converse(*converse(a36)) & 
     a58 E *converse(*converse(a36))
      & p1(a57) = p1(a58)
2:  #function(a21,a18,a36)


|-

1:  p2(a57) = p2(a58)


 by 853

Line 853:  
----------Proved---------
1:  a58 E *converse(*converse(a36))
      & p1(a57) = p1(a58)
2:  #function(a21,a18,a36)
3:  a57 E *converse(*converse(a36))


|-

1:  p2(a57) = p2(a58)


 by 854

Line 854:  
----------Proved---------
1:  a57 E *converse(*converse(a36))
2:  a58 E *converse(*converse(a36))
3:  p1(a57) = p1(a58)
4:  #function(a21,a18,a36)


|-

1:  p2(a57) = p2(a58)


 by 855

Line 855:  
----------Proved---------
1:  <p2(a57),p1(a57)> E *converse(a36)
2:  a58 E *converse(*converse(a36))
3:  p1(a57) = p1(a58)
4:  #function(a21,a18,a36)


|-

1:  p2(a57) = p2(a58)


 by 856

Line 856:  
----------Proved---------
1:  a58 E *converse(*converse(a36))
2:  p1(a57) = p1(a58)
3:  #function(a21,a18,a36)
4:  a57 E a36


|-

1:  p2(a57) = p2(a58)


 by 857

Line 857:  
----------Proved---------
1:  <p2(a58),p1(a58)> E *converse(a36)
2:  p1(a57) = p1(a58)
3:  #function(a21,a18,a36)
4:  a57 E a36


|-

1:  p2(a57) = p2(a58)


 by 858

Line 858:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  a57 E a36
3:  a58 E a36
4:  p1(a57) = p1(a58)


|-

1:  p2(a57) = p2(a58)


 by 859

Line 859:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a57 E a36
3:  a58 E a36
4:  p1(a57) = p1(a58)


|-

1:  p2(a57) = p2(a58)


 by 860

Line 860:  
----------Proved---------
1:  (Ax12.(Ax16.x12 E a36
      & x16 E a36 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))
2:  a57 E a36
3:  a58 E a36
4:  p1(a57) = p1(a58)


|-

1:  p2(a57) = p2(a58)


 by 861

Line 861:  
----------Proved---------
1:  (Ax24.a57 E a36
      & x24 E a36 & p1(a57) = p1(x24)
      -> p2(a57) = p2(x24))
2:  a57 E a36
3:  a58 E a36
4:  p1(a57) = p1(a58)


|-

1:  p2(a57) = p2(a58)


 by 862

Line 862:  
----------Proved---------
1:  a57 E a36
      & a58 E a36 & p1(a57) = p1(a58)
      -> p2(a57) = p2(a58)
2:  a57 E a36
3:  a58 E a36
4:  p1(a57) = p1(a58)


|-

1:  p2(a57) = p2(a58)


 by 864, 863

Line 864:  
----------Proved---------
1:  p2(a57) = p2(a58)


|-

1:  p2(a57) = p2(a58)




Line 863:  
----------Proved---------
1:  a57 E a36
2:  a58 E a36
3:  p1(a57) = p1(a58)


|-

1:  a57 E a36
      & a58 E a36 & p1(a57) = p1(a58)


 by 866, 865

Line 866:  
----------Proved---------
1:  a58 E a36
2:  p1(a57) = p1(a58)


|-

1:  a58 E a36 & p1(a57) = p1(a58)


 by 868, 867

Line 868:  
----------Proved---------
1:  p1(a57) = p1(a58)


|-

1:  p1(a57) = p1(a58)




Line 867:  
----------Proved---------
1:  a58 E a36


|-

1:  a58 E a36




Line 865:  
----------Proved---------
1:  a57 E a36


|-

1:  a57 E a36




Line 824:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  #relation(a21,a18,*converse(*converse(a36)))
      & (Ax6.
     x6 E a21
      -> (Ex10.<x6,x10> E *converse(*converse(a36))))


 by 827, 826

Line 827:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E *converse(*converse(a36))))


 by 838

Line 838:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  a55 E a21
      -> (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 839

Line 839:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  a55 E a21


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 840

Line 840:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a55 E a21


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 841

Line 841:  
----------Proved---------
1:  #relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36))
2:  a55 E a21


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 842

Line 842:  
----------Proved---------
1:  (Ax6.x6 E a21 -> (Ex10.<x6,x10> E a36))
2:  a55 E a21


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 843

Line 843:  
----------Proved---------
1:  a55 E a21 -> (Ex22.<a55,x22> E a36)
2:  a55 E a21


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 845, 844

Line 845:  
----------Proved---------
1:  (Ex22.<a55,x22> E a36)


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 846

Line 846:  
----------Proved---------
1:  <a55,a56> E a36


|-

1:  (Ex21.<a55,x21> E *converse(*converse(a36)))


 by 847

Line 847:  
----------Proved---------
1:  <a55,a56> E a36


|-

1:  <a55,a56> E *converse(*converse(a36))


 by 848

Line 848:  
----------Proved---------
1:  <a55,a56> E a36


|-

1:  <a56,a55> E *converse(a36)


 by 849

Line 849:  
----------Proved---------
1:  <a55,a56> E a36


|-

1:  <a55,a56> E a36




Line 844:  
----------Proved---------
1:  a55 E a21


|-

1:  a55 E a21




Line 826:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  #relation(a21,a18,*converse(*converse(a36)))


 by 828

Line 828:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  (Ax5.x5 E *converse(*converse(a36)) -> p1(x5) E a21
      & p2(x5) E a18)


 by 829

Line 829:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  a54 E *converse(*converse(a36)) -> p1(a54) E a21
      & p2(a54) E a18


 by 830

Line 830:  
----------Proved---------
1:  a54 E *converse(*converse(a36))
2:  #function(a21,a18,a36)


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 831

Line 831:  
----------Proved---------
1:  <p2(a54),p1(a54)> E *converse(a36)
2:  #function(a21,a18,a36)


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 832

Line 832:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  a54 E a36


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 833

Line 833:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a54 E a36


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 834

Line 834:  
----------Proved---------
1:  #relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36))
2:  a54 E a36


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 835

Line 835:  
----------Proved---------
1:  #relation(a21,a18,a36)
2:  a54 E a36


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 836

Line 836:  
----------Proved---------
1:  (Ax5.x5 E a36
      -> p1(x5) E a21 & p2(x5) E a18)
2:  a54 E a36


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by 837

Line 837:  
----------Proved---------
1:  a54 E a36
      -> p1(a54) E a21 & p2(a54) E a18
2:  a54 E a36


|-

1:  p1(a54) E a21 & p2(a54) E a18


 by MP

Line 683:  
----------Proved---------
1:  *converse(*setdiff(a36,*sing(<a37,a20>))) = *setdiff(*converse(a36),*sing(<a20,a37>))
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
5:  #function(a21,a18,*converse(*converse(a36)))
6:  #function(a18,a21,*converse(a36))
7:  <a37,a20> E *converse(*converse(a36))
8:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
9:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 685

Line 685:  
----------Proved---------
1:  (Ax1.*converse(*setdiff(a36,*sing(<a37,a20>))) E x1
      == *setdiff(*converse(a36),*sing(<a20,a37>)) E x1)
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
5:  #function(a21,a18,*converse(*converse(a36)))
6:  #function(a18,a21,*converse(a36))
7:  <a37,a20> E *converse(*converse(a36))
8:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
9:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 686

Line 686:  
----------Proved---------
1:  
     *converse(*setdiff(a36,*sing(<a37,a20>))) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}
      == *setdiff(*converse(a36),*sing(<a20,a37>)) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
5:  #function(a21,a18,*converse(*converse(a36)))
6:  #function(a18,a21,*converse(a36))
7:  <a37,a20> E *converse(*converse(a36))
8:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
9:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 687

Line 687:  
----------Proved---------
1:  
     (
     *converse(*setdiff(a36,*sing(<a37,a20>))) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}
      -> *setdiff(*converse(a36),*sing(<a20,a37>)) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)})
      & (
     *setdiff(*converse(a36),*sing(<a20,a37>)) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}
      -> *converse(*setdiff(a36,*sing(<a37,a20>))) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)})
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
5:  #function(a21,a18,*converse(*converse(a36)))
6:  #function(a18,a21,*converse(a36))
7:  <a37,a20> E *converse(*converse(a36))
8:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
9:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 688

Line 688:  
----------Proved---------
1:  
     *setdiff(*converse(a36),*sing(<a20,a37>)) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}
      -> *converse(*setdiff(a36,*sing(<a37,a20>))) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
5:  #function(a21,a18,*converse(*converse(a36)))
6:  #function(a18,a21,*converse(a36))
7:  <a37,a20> E *converse(*converse(a36))
8:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
9:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 690, 689

Line 690:  
----------Proved---------
1:  *converse(*setdiff(a36,*sing(<a37,a20>))) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


 by 822

Line 822:  
----------Proved---------
1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*converse(*setdiff(a36,*sing(<a37,a20>))))




Line 689:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
4:  #function(a21,a18,*converse(*converse(a36)))
5:  #function(a18,a21,*converse(a36))
6:  <a37,a20> E *converse(*converse(a36))
7:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
8:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  *setdiff(*converse(a36),*sing(<a20,a37>)) E {x1|#function(a19,*imageb(*converse(a36),a19),x1)}


 by 691

Line 691:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
4:  #function(a21,a18,*converse(*converse(a36)))
5:  #function(a18,a21,*converse(a36))
6:  <a37,a20> E *converse(*converse(a36))
7:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
8:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 693, 692

Line 693:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))


 by 703, 702

Line 703:  
----------Proved---------


|-

1:  (Ax1.(Ax2.(Ax3.x3 E x1 == x3 E x2)
      -> (Ax3.(Ax4.
     #function(x1,x3,x4) == #function(x2,x3,x4)))))


 by 762

Line 762:  
----------Proved---------


|-

1:  (Ax5.(Ax10.x10 E a47 == x10 E x5) -> (Ax11.(Ax13.
     #function(a47,x11,x13)
      == #function(x5,x11,x13))))


 by 763

Line 763:  
----------Proved---------


|-

1:  
     (Ax14.x14 E a47 == x14 E a48) -> (Ax15.(Ax17.
     #function(a47,x15,x17)
      == #function(a48,x15,x17)))


 by 764

Line 764:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax15.(Ax17.#function(a47,x15,x17) == #function(a48,x15,x17)))


 by 765

Line 765:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax18.#function(a47,a49,x18) == #function(a48,a49,x18))


 by 766

Line 766:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #function(a47,a49,a50) == #function(a48,a49,a50)


 by 767

Line 767:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  
     (#function(a47,a49,a50) -> #function(a48,a49,a50)) & (
     #function(a48,a49,a50)
      -> #function(a47,a49,a50))


 by 769, 768

Line 769:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #function(a48,a49,a50) -> #function(a47,a49,a50)


 by 814, 813

Line 814:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax1.x1 E a48 == x1 E a47)


 by 815

Line 815:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  a53 E a48 == a53 E a47


 by 816

Line 816:  
----------Proved---------
1:  a53 E a47 == a53 E a48


|-

1:  a53 E a48 == a53 E a47


 by 817

Line 817:  
----------Proved---------
1:  (a53 E a47 -> a53 E a48) & (
     a53 E a48 -> a53 E a47)


|-

1:  a53 E a48 == a53 E a47


 by 818

Line 818:  
----------Proved---------
1:  a53 E a47 -> a53 E a48
2:  a53 E a48 -> a53 E a47


|-

1:  a53 E a48 == a53 E a47


 by 819

Line 819:  
----------Proved---------
1:  a53 E a47 -> a53 E a48
2:  a53 E a48 -> a53 E a47


|-

1:  (a53 E a48 -> a53 E a47) & (
     a53 E a47 -> a53 E a48)


 by 821, 820

Line 821:  
----------Proved---------
1:  a53 E a47 -> a53 E a48


|-

1:  a53 E a47 -> a53 E a48




Line 820:  
----------Proved---------
1:  a53 E a48 -> a53 E a47


|-

1:  a53 E a48 -> a53 E a47




Line 813:  
----------Proved---------
1:  (Ax1.x1 E a48 == x1 E a47)


|-

1:  #function(a48,a49,a50) -> #function(a47,a49,a50)


 by ExtFun


Proof of lemma ExtFun starts:


Line ExtFun.768:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #function(a47,a49,a50) -> #function(a48,a49,a50)


 by ExtFun.770

Line ExtFun.770:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #function(a48,a49,a50)


 by ExtFun.771

Line ExtFun.771:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  
     (#relation(a48,a49,a50) & (Ax6.x6 E a48
      -> (Ex10.<x6,x10> E a50)))
      & (Ax12.(Ax16.
     x12 E a50 & x16 E a50
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


 by ExtFun.773, 772

Line ExtFun.773:  
----------Proved---------
1:  #function(a47,a49,a50)


|-

1:  (Ax12.(Ax16.x12 E a50
      & x16 E a50 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))


 by ExtFun.811

Line ExtFun.811:  
----------Proved---------
1:  
     (#relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50)))
      & (Ax12.(Ax16.
     x12 E a50 & x16 E a50
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  (Ax12.(Ax16.x12 E a50
      & x16 E a50 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))


 by ExtFun.812

Line ExtFun.812:  
----------Proved---------
1:  (Ax12.(Ax16.x12 E a50
      & x16 E a50 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))


|-

1:  (Ax12.(Ax16.x12 E a50
      & x16 E a50 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))




Line ExtFun.772:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #relation(a48,a49,a50) & (Ax6.x6 E a48
      -> (Ex10.<x6,x10> E a50))


 by ExtFun.775, 774

Line ExtFun.775:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax6.x6 E a48 -> (Ex10.<x6,x10> E a50))


 by ExtFun.800

Line ExtFun.800:  
----------Proved---------
1:  
     (#relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50)))
      & (Ax12.(Ax16.
     x12 E a50 & x16 E a50
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax6.x6 E a48 -> (Ex10.<x6,x10> E a50))


 by ExtFun.801

Line ExtFun.801:  
----------Proved---------
1:  #relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50))
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax6.x6 E a48 -> (Ex10.<x6,x10> E a50))


 by ExtFun.802

Line ExtFun.802:  
----------Proved---------
1:  (Ax6.x6 E a47 -> (Ex10.<x6,x10> E a50))
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax6.x6 E a48 -> (Ex10.<x6,x10> E a50))


 by ExtFun.803

Line ExtFun.803:  
----------Proved---------
1:  (Ax6.x6 E a47 -> (Ex10.<x6,x10> E a50))
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  a52 E a48 -> (Ex19.<a52,x19> E a50)


 by ExtFun.804

Line ExtFun.804:  
----------Proved---------
1:  a52 E a47 -> (Ex20.<a52,x20> E a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  a52 E a48 -> (Ex19.<a52,x19> E a50)


 by ExtFun.805

Line ExtFun.805:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)
2:  a52 E a48
3:  a52 E a47 -> (Ex20.<a52,x20> E a50)


|-

1:  (Ex19.<a52,x19> E a50)


 by ExtFun.806

Line ExtFun.806:  
----------Proved---------
1:  a52 E a47 == a52 E a48
2:  a52 E a48
3:  a52 E a47 -> (Ex20.<a52,x20> E a50)


|-

1:  (Ex19.<a52,x19> E a50)


 by ExtFun.807

Line ExtFun.807:  
----------Proved---------
1:  (a52 E a47 -> a52 E a48) & (
     a52 E a48 -> a52 E a47)
2:  a52 E a48
3:  a52 E a47 -> (Ex20.<a52,x20> E a50)


|-

1:  (Ex19.<a52,x19> E a50)


 by ExtFun.808

Line ExtFun.808:  
----------Proved---------
1:  a52 E a48 -> a52 E a47
2:  a52 E a48
3:  a52 E a47 -> (Ex20.<a52,x20> E a50)


|-

1:  (Ex19.<a52,x19> E a50)


 by ExtFun.810, 809

Line ExtFun.810:  
----------Proved---------
1:  a52 E a47 -> (Ex20.<a52,x20> E a50)
2:  a52 E a47


|-

1:  (Ex19.<a52,x19> E a50)


 by ExtFun.MP


Proof of lemma ExtFun.MP starts:


Line ExtFun.MP.3:  
----------Proved---------
1:  P1 -> P2
2:  P1


|-

1:  P2


 by ExtFun.MP.5, 4

Line ExtFun.MP.5:  
----------Proved---------
1:  P2
2:  P1


|-

1:  P2




Line ExtFun.MP.4:  
----------Proved---------
1:  P1


|-

1:  P1
2:  P2





Proof of lemma ExtFun.MP ends


Line ExtFun.809:  
----------Proved---------
1:  a52 E a48


|-

1:  a52 E a48




Line ExtFun.774:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #relation(a48,a49,a50)


 by ExtFun.776

Line ExtFun.776:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  (Ax5.x5 E a50
      -> p1(x5) E a48 & p2(x5) E a49)


 by ExtFun.777

Line ExtFun.777:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  a51 E a50
      -> p1(a51) E a48 & p2(a51) E a49


 by ExtFun.778

Line ExtFun.778:  
----------Proved---------
1:  a51 E a50
2:  #function(a47,a49,a50)
3:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  p1(a51) E a48 & p2(a51) E a49


 by ExtFun.780, 779

Line ExtFun.780:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  a51 E a50


|-

1:  p2(a51) E a49


 by ExtFun.792

Line ExtFun.792:  
----------Proved---------
1:  
     (#relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50)))
      & (Ax12.(Ax16.
     x12 E a50 & x16 E a50
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a51 E a50


|-

1:  p2(a51) E a49


 by ExtFun.793

Line ExtFun.793:  
----------Proved---------
1:  #relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50))
2:  a51 E a50


|-

1:  p2(a51) E a49


 by ExtFun.794

Line ExtFun.794:  
----------Proved---------
1:  #relation(a47,a49,a50)
2:  a51 E a50


|-

1:  p2(a51) E a49


 by ExtFun.795

Line ExtFun.795:  
----------Proved---------
1:  (Ax5.x5 E a50
      -> p1(x5) E a47 & p2(x5) E a49)
2:  a51 E a50


|-

1:  p2(a51) E a49


 by ExtFun.796

Line ExtFun.796:  
----------Proved---------
1:  a51 E a50
      -> p1(a51) E a47 & p2(a51) E a49
2:  a51 E a50


|-

1:  p2(a51) E a49


 by ExtFun.798, 797

Line ExtFun.798:  
----------Proved---------
1:  p1(a51) E a47 & p2(a51) E a49


|-

1:  p2(a51) E a49


 by ExtFun.799

Line ExtFun.799:  
----------Proved---------
1:  p2(a51) E a49


|-

1:  p2(a51) E a49




Line ExtFun.797:  
----------Proved---------
1:  a51 E a50


|-

1:  a51 E a50




Line ExtFun.779:  
----------Proved---------
1:  #function(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)
3:  a51 E a50


|-

1:  p1(a51) E a48


 by ExtFun.781

Line ExtFun.781:  
----------Proved---------
1:  
     (#relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50)))
      & (Ax12.(Ax16.
     x12 E a50 & x16 E a50
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  (Ax14.x14 E a47 == x14 E a48)
3:  a51 E a50


|-

1:  p1(a51) E a48


 by ExtFun.782

Line ExtFun.782:  
----------Proved---------
1:  #relation(a47,a49,a50) & (Ax6.x6 E a47
      -> (Ex10.<x6,x10> E a50))
2:  (Ax14.x14 E a47 == x14 E a48)
3:  a51 E a50


|-

1:  p1(a51) E a48


 by ExtFun.783

Line ExtFun.783:  
----------Proved---------
1:  #relation(a47,a49,a50)
2:  (Ax14.x14 E a47 == x14 E a48)
3:  a51 E a50


|-

1:  p1(a51) E a48


 by ExtFun.784

Line ExtFun.784:  
----------Proved---------
1:  (Ax5.x5 E a50
      -> p1(x5) E a47 & p2(x5) E a49)
2:  (Ax14.x14 E a47 == x14 E a48)
3:  a51 E a50


|-

1:  p1(a51) E a48


 by ExtFun.785

Line ExtFun.785:  
----------Proved---------
1:  a51 E a50
      -> p1(a51) E a47 & p2(a51) E a49
2:  (Ax14.x14 E a47 == x14 E a48)
3:  a51 E a50


|-

1:  p1(a51) E a48


 by ExtFun.787, 786

Line ExtFun.787:  
----------Proved---------
1:  p1(a51) E a47 & p2(a51) E a49
2:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  p1(a51) E a48


 by ExtFun.788

Line ExtFun.788:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)
2:  p1(a51) E a47


|-

1:  p1(a51) E a48


 by ExtFun.789

Line ExtFun.789:  
----------Proved---------
1:  p1(a51) E a47 == p1(a51) E a48
2:  p1(a51) E a47


|-

1:  p1(a51) E a48


 by ExtFun.790

Line ExtFun.790:  
----------Proved---------
1:  
     (p1(a51) E a47 -> p1(a51) E a48) & (p1(a51) E a48
      -> p1(a51) E a47)
2:  p1(a51) E a47


|-

1:  p1(a51) E a48


 by ExtFun.791

Line ExtFun.791:  
----------Proved---------
1:  p1(a51) E a47 -> p1(a51) E a48
2:  p1(a51) E a47


|-

1:  p1(a51) E a48


 by ExtFun.MP

Line ExtFun.786:  
----------Proved---------
1:  a51 E a50


|-

1:  a51 E a50





Proof of lemma ExtFun ends


Line 768:  
----------Proved---------
1:  (Ax14.x14 E a47 == x14 E a48)


|-

1:  #function(a47,a49,a50) -> #function(a48,a49,a50)


 by ExtFun

Line 702:  
----------Proved---------
1:  (Ax1.(Ax2.(Ax3.x3 E x1 == x3 E x2)
      -> (Ax3.(Ax4.
     #function(x1,x3,x4) == #function(x2,x3,x4)))))
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))


 by 705, 704

Line 705:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  (Ax1.x1 E a19
      == x1 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))


 by 710

Line 710:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  a43 E a19
      == a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))


 by 711

Line 711:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  
     (a43 E a19
      -> a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))) & (
     a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))
      -> a43 E a19)


 by 713, 712

Line 713:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  
     a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))
      -> a43 E a19


 by 738

Line 738:  
----------Proved---------
1:  a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))
2:  #function(a21,a18,a36)


|-

1:  a43 E a19


 by 739

Line 739:  
----------Proved---------
1:  (Ex11.x11 E *imageb(*converse(a36),a19)
      & <x11,a43> E *converse(*converse(a36)))
2:  #function(a21,a18,a36)


|-

1:  a43 E a19


 by 740

Line 740:  
----------Proved---------
1:  a45 E *imageb(*converse(a36),a19)
      & <a45,a43> E *converse(*converse(a36))
2:  #function(a21,a18,a36)


|-

1:  a43 E a19


 by 741

Line 741:  
----------Proved---------
1:  a45 E *imageb(*converse(a36),a19)
2:  <a45,a43> E *converse(*converse(a36))
3:  #function(a21,a18,a36)


|-

1:  a43 E a19


 by 742

Line 742:  
----------Proved---------
1:  (Ex12.x12 E a19 & <x12,a45> E *converse(a36))
2:  <a45,a43> E *converse(*converse(a36))
3:  #function(a21,a18,a36)


|-

1:  a43 E a19


 by 743

Line 743:  
----------Proved---------
1:  a46 E a19 & <a46,a45> E *converse(a36)
2:  <a45,a43> E *converse(*converse(a36))
3:  #function(a21,a18,a36)


|-

1:  a43 E a19


 by 744

Line 744:  
----------Proved---------
1:  <a46,a45> E *converse(a36)
2:  <a45,a43> E *converse(*converse(a36))
3:  #function(a21,a18,a36)
4:  a46 E a19


|-

1:  a43 E a19


 by 745

Line 745:  
----------Proved---------
1:  <a45,a43> E *converse(*converse(a36))
2:  #function(a21,a18,a36)
3:  a46 E a19
4:  <a45,a46> E a36


|-

1:  a43 E a19


 by 746

Line 746:  
----------Proved---------
1:  <a43,a45> E *converse(a36)
2:  #function(a21,a18,a36)
3:  a46 E a19
4:  <a45,a46> E a36


|-

1:  a43 E a19


 by 747

Line 747:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  a46 E a19
3:  <a45,a46> E a36
4:  <a45,a43> E a36


|-

1:  a43 E a19


 by 748

Line 748:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a46 E a19
3:  <a45,a46> E a36
4:  <a45,a43> E a36


|-

1:  a43 E a19


 by 749

Line 749:  
----------Proved---------
1:  (Ax12.(Ax16.x12 E a36
      & x16 E a36 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))
2:  a46 E a19
3:  <a45,a46> E a36
4:  <a45,a43> E a36


|-

1:  a43 E a19


 by 750

Line 750:  
----------Proved---------
1:  (Ax17.<a45,a46> E a36
      & x17 E a36 & a45 = p1(x17)
      -> a46 = p2(x17))
2:  a46 E a19
3:  <a45,a46> E a36
4:  <a45,a43> E a36


|-

1:  a43 E a19


 by 751

Line 751:  
----------Proved---------
1:  <a45,a46> E a36
      & <a45,a43> E a36 & a45 = a45
      -> a46 = a43
2:  a46 E a19
3:  <a45,a46> E a36
4:  <a45,a43> E a36


|-

1:  a43 E a19


 by 753, 752

Line 753:  
----------Proved---------
1:  a46 = a43
2:  a46 E a19


|-

1:  a43 E a19


 by 758

Line 758:  
----------Proved---------
1:  (Ax1.a46 E x1 == a43 E x1)
2:  a46 E a19


|-

1:  a43 E a19


 by 759

Line 759:  
----------Proved---------
1:  a46 E a19 == a43 E a19
2:  a46 E a19


|-

1:  a43 E a19


 by 760

Line 760:  
----------Proved---------
1:  (a46 E a19 -> a43 E a19) & (
     a43 E a19 -> a46 E a19)
2:  a46 E a19


|-

1:  a43 E a19


 by 761

Line 761:  
----------Proved---------
1:  a46 E a19 -> a43 E a19
2:  a46 E a19


|-

1:  a43 E a19


 by MP

Line 752:  
----------Proved---------
1:  <a45,a46> E a36
2:  <a45,a43> E a36


|-

1:  <a45,a46> E a36
      & <a45,a43> E a36 & a45 = a45


 by 755, 754

Line 755:  
----------Proved---------
1:  <a45,a43> E a36


|-

1:  <a45,a43> E a36 & a45 = a45


 by 757, 756

Line 757:  
----------Proved---------


|-

1:  a45 = a45


 by REFLEQ

Line 756:  
----------Proved---------
1:  <a45,a43> E a36


|-

1:  <a45,a43> E a36




Line 754:  
----------Proved---------
1:  <a45,a46> E a36


|-

1:  <a45,a46> E a36




Line 712:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  a43 E a19
      -> a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))


 by 714

Line 714:  
----------Proved---------
1:  a43 E a19
2:  a18 = *union(a19,*sing(a20))
3:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))


|-

1:  a43 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19))


 by 715

Line 715:  
----------Proved---------
1:  (Ax6.x6 E a18 -> (Ex10.<x6,x10> E *converse(a36)))
2:  a43 E a19
3:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex19.x19 E *imageb(*converse(a36),a19)
      & <x19,a43> E *converse(*converse(a36)))


 by 716

Line 716:  
----------Proved---------
1:  a43 E a18 -> (Ex20.<a43,x20> E *converse(a36))
2:  a43 E a19
3:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex19.x19 E *imageb(*converse(a36),a19)
      & <x19,a43> E *converse(*converse(a36)))


 by 718, 717

Line 718:  
----------Proved---------
1:  (Ex20.<a43,x20> E *converse(a36))
2:  a43 E a19


|-

1:  (Ex19.x19 E *imageb(*converse(a36),a19)
      & <x19,a43> E *converse(*converse(a36)))


 by 729

Line 729:  
----------Proved---------
1:  <a43,a44> E *converse(a36)
2:  a43 E a19


|-

1:  (Ex19.x19 E *imageb(*converse(a36),a19)
      & <x19,a43> E *converse(*converse(a36)))


 by 730

Line 730:  
----------Proved---------
1:  <a43,a44> E *converse(a36)
2:  a43 E a19


|-

1:  a44 E *imageb(*converse(a36),a19)
      & <a44,a43> E *converse(*converse(a36))


 by 732, 731

Line 732:  
----------Proved---------
1:  <a43,a44> E *converse(a36)


|-

1:  <a44,a43> E *converse(*converse(a36))


 by 737

Line 737:  
----------Proved---------
1:  <a43,a44> E *converse(a36)


|-

1:  <a43,a44> E *converse(a36)




Line 731:  
----------Proved---------
1:  <a43,a44> E *converse(a36)
2:  a43 E a19


|-

1:  a44 E *imageb(*converse(a36),a19)


 by 733

Line 733:  
----------Proved---------
1:  <a43,a44> E *converse(a36)
2:  a43 E a19


|-

1:  (Ex10.x10 E a19 & <x10,a44> E *converse(a36))


 by 734

Line 734:  
----------Proved---------
1:  <a43,a44> E *converse(a36)
2:  a43 E a19


|-

1:  a43 E a19 & <a43,a44> E *converse(a36)


 by 736, 735

Line 736:  
----------Proved---------
1:  <a43,a44> E *converse(a36)


|-

1:  <a43,a44> E *converse(a36)




Line 735:  
----------Proved---------
1:  a43 E a19


|-

1:  a43 E a19




Line 717:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  a43 E a19


|-

1:  a43 E a18


 by 719

Line 719:  
----------Proved---------
1:  (Ax1.a18 E x1 == *union(a19,*sing(a20)) E x1)
2:  a43 E a19


|-

1:  a43 E a18


 by 720

Line 720:  
----------Proved---------
1:  a18 E {x1|a43 E x1}
      == *union(a19,*sing(a20)) E {x1|a43 E x1}
2:  a43 E a19


|-

1:  a43 E a18


 by 721

Line 721:  
----------Proved---------
1:  
     (a18 E {x1|a43 E x1}
      -> *union(a19,*sing(a20)) E {x1|a43 E x1}) & (
     *union(a19,*sing(a20)) E {x1|a43 E x1}
      -> a18 E {x1|a43 E x1})
2:  a43 E a19


|-

1:  a43 E a18


 by 722

Line 722:  
----------Proved---------
1:  *union(a19,*sing(a20)) E {x1|a43 E x1}
      -> a18 E {x1|a43 E x1}
2:  a43 E a19


|-

1:  a43 E a18


 by 724, 723

Line 724:  
----------Proved---------
1:  a18 E {x1|a43 E x1}


|-

1:  a43 E a18


 by 728

Line 728:  
----------Proved---------
1:  a43 E a18


|-

1:  a43 E a18




Line 723:  
----------Proved---------
1:  a43 E a19


|-

1:  *union(a19,*sing(a20)) E {x1|a43 E x1}


 by 725

Line 725:  
----------Proved---------
1:  a43 E a19


|-

1:  a43 E *union(a19,*sing(a20))


 by 726

Line 726:  
----------Proved---------
1:  a43 E a19


|-

1:  a43 E a19 v a43 E *sing(a20)


 by 727

Line 727:  
----------Proved---------
1:  a43 E a19


|-

1:  a43 E a19




Line 704:  
----------Proved---------
1:  (Ax1.(Ax2.(Ax3.x3 E x1 == x3 E x2)
      -> (Ax3.(Ax4.
     #function(x1,x3,x4) == #function(x2,x3,x4)))))
2:  (Ax1.x1 E a19
      == x1 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))


|-

1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))


 by 706

Line 706:  
----------Proved---------
1:  (Ax6.(Ax11.x11 E a19 == x11 E x6) -> (Ax12.(Ax14.
     #function(a19,x12,x14)
      == #function(x6,x12,x14))))
2:  (Ax1.x1 E a19
      == x1 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))


|-

1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))


 by 707

Line 707:  
----------Proved---------
1:  
     (Ax15.x15 E a19
      == x15 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))
      -> (Ax16.(Ax18.
     #function(a19,x16,x18)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x16,x18)))
2:  (Ax1.x1 E a19
      == x1 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))


|-

1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))


 by 709, 708

Line 709:  
----------Proved---------
1:  (Ax16.(Ax18.#function(a19,x16,x18)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x16,x18)))


|-

1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))




Line 708:  
----------Proved---------
1:  (Ax1.x1 E a19
      == x1 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))


|-

1:  (Ax15.x15 E a19
      == x15 E *imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)))




Line 692:  
----------Proved---------
1:  (Ax1.(Ax2.#function(a19,x1,x2)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),x1,x2)))
2:  #function(a21,a18,*converse(*converse(a36)))
3:  #function(a18,a21,*converse(a36))
4:  <a37,a20> E *converse(*converse(a36))
5:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
6:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 694

Line 694:  
----------Proved---------
1:  (Ax3.#function(a19,*imageb(*converse(a36),a19),x3)
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),x3))
2:  #function(a21,a18,*converse(*converse(a36)))
3:  #function(a18,a21,*converse(a36))
4:  <a37,a20> E *converse(*converse(a36))
5:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
6:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 695

Line 695:  
----------Proved---------
1:  
     #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))
      == #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))
2:  #function(a21,a18,*converse(*converse(a36)))
3:  #function(a18,a21,*converse(a36))
4:  <a37,a20> E *converse(*converse(a36))
5:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
6:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 696

Line 696:  
----------Proved---------
1:  
     (
     #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))
      -> #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>))))
      & (
     #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))
      -> #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>))))
2:  #function(a21,a18,*converse(*converse(a36)))
3:  #function(a18,a21,*converse(a36))
4:  <a37,a20> E *converse(*converse(a36))
5:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
6:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 697

Line 697:  
----------Proved---------
1:  
     #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))
      -> #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))
2:  #function(a21,a18,*converse(*converse(a36)))
3:  #function(a18,a21,*converse(a36))
4:  <a37,a20> E *converse(*converse(a36))
5:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
6:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 699, 698

Line 699:  
----------Proved---------
1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


|-

1:  #function(a19,*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))




Line 698:  
----------Proved---------
1:  #function(a21,a18,*converse(*converse(a36)))
2:  #function(a18,a21,*converse(a36))
3:  <a37,a20> E *converse(*converse(a36))
4:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
5:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 700

Line 700:  
----------Proved---------
1:  
     (#relation(a21,a18,*converse(*converse(a36)))
      & (Ax6.
     x6 E a21
      -> (Ex10.<x6,x10> E *converse(*converse(a36))))) & (Ax12.(Ax16.
     x12 E *converse(*converse(a36)) & 
     x16 E *converse(*converse(a36))
      & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))
2:  #function(a18,a21,*converse(a36))
3:  <a37,a20> E *converse(*converse(a36))
4:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
5:  ~a37 E *imageb(*converse(a36),a19)


|-

1:  #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by 701

Line 701:  
----------Proved---------
1:  ~a37 E *imageb(*converse(a36),a19)
2:  a21 = *union(*imageb(*converse(a36),a19),*sing(a37))
3:  #function(a18,a21,*converse(a36))
4:  <a37,a20> E *converse(*converse(a36))
5:  (Ax12.(Ax16.
     x12 E *converse(*converse(a36)) & 
     x16 E *converse(*converse(a36))
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(*imageb(*converse(*converse(a36)),*imageb(*converse(a36),a19)),*imageb(*converse(a36),a19),*setdiff(*converse(a36),*sing(<a20,a37>)))


 by FunctionLemma2


Proof of lemma FunctionLemma2 starts:


Line FunctionLemma2.578:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(*imageb(*converse(a36),a19),a19,*setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2.580

Line FunctionLemma2.580:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  
     (
     #relation(*imageb(*converse(a36),a19),a19,*setdiff(a36,*sing(<a37,a20>)))
      & (Ax6.
     x6 E *imageb(*converse(a36),a19)
      -> (Ex10.<x6,x10> E *setdiff(a36,*sing(<a37,a20>))))) & (Ax12.(Ax16.
     x12 E *setdiff(a36,*sing(<a37,a20>)) & 
     x16 E *setdiff(a36,*sing(<a37,a20>))
      & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))


 by FunctionLemma2.582, 581

Line FunctionLemma2.582:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  (Ax12.(Ax16.
     x12 E *setdiff(a36,*sing(<a37,a20>)) & 
     x16 E *setdiff(a36,*sing(<a37,a20>))
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


 by FunctionLemma2.654

Line FunctionLemma2.654:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  (Ax17.
     a41 E *setdiff(a36,*sing(<a37,a20>)) & 
     x17 E *setdiff(a36,*sing(<a37,a20>))
      & p1(a41) = p1(x17) -> p2(a41) = p2(x17))


 by FunctionLemma2.655

Line FunctionLemma2.655:  
----------Proved---------
1:  #function(a21,a18,a36)


|-

1:  
     a41 E *setdiff(a36,*sing(<a37,a20>)) & 
     a42 E *setdiff(a36,*sing(<a37,a20>))
      & p1(a41) = p1(a42) -> p2(a41) = p2(a42)


 by FunctionLemma2.656

Line FunctionLemma2.656:  
----------Proved---------
1:  a41 E *setdiff(a36,*sing(<a37,a20>)) & 
     a42 E *setdiff(a36,*sing(<a37,a20>))
      & p1(a41) = p1(a42)
2:  #function(a21,a18,a36)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.657

Line FunctionLemma2.657:  
----------Proved---------
1:  a42 E *setdiff(a36,*sing(<a37,a20>))
      & p1(a41) = p1(a42)
2:  #function(a21,a18,a36)
3:  a41 E *setdiff(a36,*sing(<a37,a20>))


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.658

Line FunctionLemma2.658:  
----------Proved---------
1:  a41 E *setdiff(a36,*sing(<a37,a20>))
2:  a42 E *setdiff(a36,*sing(<a37,a20>))
3:  p1(a41) = p1(a42)
4:  #function(a21,a18,a36)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.659

Line FunctionLemma2.659:  
----------Proved---------
1:  a41 E a36 & ~a41 E *sing(<a37,a20>)
2:  a42 E *setdiff(a36,*sing(<a37,a20>))
3:  p1(a41) = p1(a42)
4:  #function(a21,a18,a36)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.660

Line FunctionLemma2.660:  
----------Proved---------
1:  a42 E *setdiff(a36,*sing(<a37,a20>))
2:  p1(a41) = p1(a42)
3:  #function(a21,a18,a36)
4:  a41 E a36


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.661

Line FunctionLemma2.661:  
----------Proved---------
1:  a42 E a36 & ~a42 E *sing(<a37,a20>)
2:  p1(a41) = p1(a42)
3:  #function(a21,a18,a36)
4:  a41 E a36


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.662

Line FunctionLemma2.662:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  a41 E a36
3:  a42 E a36
4:  p1(a41) = p1(a42)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.663

Line FunctionLemma2.663:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a41 E a36
3:  a42 E a36
4:  p1(a41) = p1(a42)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.664

Line FunctionLemma2.664:  
----------Proved---------
1:  (Ax12.(Ax16.x12 E a36
      & x16 E a36 & p1(x12) = p1(x16)
      -> p2(x12) = p2(x16)))
2:  a41 E a36
3:  a42 E a36
4:  p1(a41) = p1(a42)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.665

Line FunctionLemma2.665:  
----------Proved---------
1:  (Ax18.a41 E a36
      & x18 E a36 & p1(a41) = p1(x18)
      -> p2(a41) = p2(x18))
2:  a41 E a36
3:  a42 E a36
4:  p1(a41) = p1(a42)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.666

Line FunctionLemma2.666:  
----------Proved---------
1:  a41 E a36
      & a42 E a36 & p1(a41) = p1(a42)
      -> p2(a41) = p2(a42)
2:  a41 E a36
3:  a42 E a36
4:  p1(a41) = p1(a42)


|-

1:  p2(a41) = p2(a42)


 by FunctionLemma2.668, 667

Line FunctionLemma2.668:  
----------Proved---------
1:  p2(a41) = p2(a42)


|-

1:  p2(a41) = p2(a42)




Line FunctionLemma2.667:  
----------Proved---------
1:  a41 E a36
2:  a42 E a36
3:  p1(a41) = p1(a42)


|-

1:  a41 E a36
      & a42 E a36 & p1(a41) = p1(a42)


 by FunctionLemma2.670, 669

Line FunctionLemma2.670:  
----------Proved---------
1:  a42 E a36
2:  p1(a41) = p1(a42)


|-

1:  a42 E a36 & p1(a41) = p1(a42)


 by FunctionLemma2.672, 671

Line FunctionLemma2.672:  
----------Proved---------
1:  p1(a41) = p1(a42)


|-

1:  p1(a41) = p1(a42)




Line FunctionLemma2.671:  
----------Proved---------
1:  a42 E a36


|-

1:  a42 E a36




Line FunctionLemma2.669:  
----------Proved---------
1:  a41 E a36


|-

1:  a41 E a36




Line FunctionLemma2.581:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  
     #relation(*imageb(*converse(a36),a19),a19,*setdiff(a36,*sing(<a37,a20>)))
      & (Ax6.
     x6 E *imageb(*converse(a36),a19)
      -> (Ex10.<x6,x10> E *setdiff(a36,*sing(<a37,a20>))))


 by FunctionLemma2.584, 583

Line FunctionLemma2.584:  
----------Proved---------
1:  ~a20 E a19


|-

1:  (Ax6.x6 E *imageb(*converse(a36),a19)
      -> (Ex10.<x6,x10> E *setdiff(a36,*sing(<a37,a20>))))


 by FunctionLemma2.632

Line FunctionLemma2.632:  
----------Proved---------
1:  ~a20 E a19


|-

1:  a39 E *imageb(*converse(a36),a19)
      -> (Ex18.<a39,x18> E *setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2.633

Line FunctionLemma2.633:  
----------Proved---------
1:  a39 E *imageb(*converse(a36),a19)
2:  ~a20 E a19


|-

1:  (Ex18.<a39,x18> E *setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2.634

Line FunctionLemma2.634:  
----------Proved---------
1:  (Ex19.x19 E a19 & <x19,a39> E *converse(a36))
2:  ~a20 E a19


|-

1:  (Ex18.<a39,x18> E *setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2.635

Line FunctionLemma2.635:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)
2:  ~a20 E a19


|-

1:  (Ex18.<a39,x18> E *setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2.636

Line FunctionLemma2.636:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)
2:  ~a20 E a19


|-

1:  <a39,a40> E *setdiff(a36,*sing(<a37,a20>))


 by FunctionLemma2.637

Line FunctionLemma2.637:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)
2:  ~a20 E a19


|-

1:  <a39,a40> E a36 & ~<a39,a40> E *sing(<a37,a20>)


 by FunctionLemma2.639, 638

Line FunctionLemma2.639:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)
2:  ~a20 E a19


|-

1:  ~<a39,a40> E *sing(<a37,a20>)


 by FunctionLemma2.642

Line FunctionLemma2.642:  
----------Proved---------
1:  <a39,a40> E *sing(<a37,a20>)
2:  a40 E a19 & <a40,a39> E *converse(a36)
3:  ~a20 E a19


|-



 by FunctionLemma2.643

Line FunctionLemma2.643:  
----------Proved---------
1:  ~a20 E a19
2:  <a39,a40> = <a37,a20>
3:  a40 E a19 & <a40,a39> E *converse(a36)


|-



 by FunctionLemma2.644

Line FunctionLemma2.644:  
----------Proved---------
1:  <a39,a40> = <a37,a20>
2:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  a20 E a19


 by FunctionLemma2.645

Line FunctionLemma2.645:  
----------Proved---------
1:  (Ax1.<a39,a40> E x1 == <a37,a20> E x1)
2:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  a20 E a19


 by FunctionLemma2.646

Line FunctionLemma2.646:  
----------Proved---------
1:  <a39,a40> E {x1|p2(x1) E a19}
      == <a37,a20> E {x1|p2(x1) E a19}
2:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  a20 E a19


 by FunctionLemma2.647

Line FunctionLemma2.647:  
----------Proved---------
1:  
     (<a39,a40> E {x1|p2(x1) E a19}
      -> <a37,a20> E {x1|p2(x1) E a19}) & (
     <a37,a20> E {x1|p2(x1) E a19}
      -> <a39,a40> E {x1|p2(x1) E a19})
2:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  a20 E a19


 by FunctionLemma2.648

Line FunctionLemma2.648:  
----------Proved---------
1:  <a39,a40> E {x1|p2(x1) E a19}
      -> <a37,a20> E {x1|p2(x1) E a19}
2:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  a20 E a19


 by FunctionLemma2.650, 649

Line FunctionLemma2.650:  
----------Proved---------
1:  <a37,a20> E {x1|p2(x1) E a19}


|-

1:  a20 E a19


 by FunctionLemma2.653

Line FunctionLemma2.653:  
----------Proved---------
1:  a20 E a19


|-

1:  a20 E a19




Line FunctionLemma2.649:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  <a39,a40> E {x1|p2(x1) E a19}


 by FunctionLemma2.651

Line FunctionLemma2.651:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  a40 E a19


 by FunctionLemma2.652

Line FunctionLemma2.652:  
----------Proved---------
1:  a40 E a19


|-

1:  a40 E a19




Line FunctionLemma2.638:  
----------Proved---------
1:  a40 E a19 & <a40,a39> E *converse(a36)


|-

1:  <a39,a40> E a36


 by FunctionLemma2.640

Line FunctionLemma2.640:  
----------Proved---------
1:  <a40,a39> E *converse(a36)


|-

1:  <a39,a40> E a36


 by FunctionLemma2.641

Line FunctionLemma2.641:  
----------Proved---------
1:  <a39,a40> E a36


|-

1:  <a39,a40> E a36




Line FunctionLemma2.583:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #relation(*imageb(*converse(a36),a19),a19,*setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2.585

Line FunctionLemma2.585:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  (Ax5.x5 E *setdiff(a36,*sing(<a37,a20>)) -> 
     p1(x5) E *imageb(*converse(a36),a19)
      & p2(x5) E a19)


 by FunctionLemma2.586

Line FunctionLemma2.586:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  #function(a21,a18,a36)
3:  <a20,a37> E *converse(a36)
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  a38 E *setdiff(a36,*sing(<a37,a20>)) -> 
     p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.587

Line FunctionLemma2.587:  
----------Proved---------
1:  a38 E *setdiff(a36,*sing(<a37,a20>))
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.588

Line FunctionLemma2.588:  
----------Proved---------
1:  a38 E a36 & ~a38 E *sing(<a37,a20>)
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.589

Line FunctionLemma2.589:  
----------Proved---------
1:  #function(a21,a18,a36)
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.590

Line FunctionLemma2.590:  
----------Proved---------
1:  
     (#relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36)))
      & (Ax12.(Ax16.
     x12 E a36 & x16 E a36
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.591

Line FunctionLemma2.591:  
----------Proved---------
1:  #relation(a21,a18,a36) & (Ax6.x6 E a21
      -> (Ex10.<x6,x10> E a36))
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.592

Line FunctionLemma2.592:  
----------Proved---------
1:  #relation(a21,a18,a36)
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.593

Line FunctionLemma2.593:  
----------Proved---------
1:  (Ax5.x5 E a36
      -> p1(x5) E a21 & p2(x5) E a18)
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.594

Line FunctionLemma2.594:  
----------Proved---------
1:  a38 E a36
      -> p1(a38) E a21 & p2(a38) E a18
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.596, 595

Line FunctionLemma2.596:  
----------Proved---------
1:  p1(a38) E a21 & p2(a38) E a18
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.597

Line FunctionLemma2.597:  
----------Proved---------
1:  p2(a38) E a18
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)
      & p2(a38) E a19


 by FunctionLemma2.599, 598

Line FunctionLemma2.599:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
3:  a38 E a36
4:  ~a38 E *sing(<a37,a20>)
5:  a18 = *union(a19,*sing(a20))
6:  p2(a38) E a18


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!


Proof of lemma FunctionLemma2.NotAgain! starts:


Line FunctionLemma2.NotAgain!.602:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
3:  a38 E a36
4:  ~a38 E *sing(<a37,a20>)
5:  a18 = *union(a19,*sing(a20))
6:  p2(a38) E a18


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.604

Line FunctionLemma2.NotAgain!.604:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))
2:  p2(a38) E a18
3:  <a37,a20> E a36
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a38 E a36
6:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.605

Line FunctionLemma2.NotAgain!.605:  
----------Proved---------
1:  (Ax1.a18 E x1 == *union(a19,*sing(a20)) E x1)
2:  p2(a38) E a18
3:  <a37,a20> E a36
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a38 E a36
6:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.606

Line FunctionLemma2.NotAgain!.606:  
----------Proved---------
1:  a18 E {x1|p2(a38) E x1}
      == *union(a19,*sing(a20)) E {x1|p2(a38) E x1}
2:  p2(a38) E a18
3:  <a37,a20> E a36
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a38 E a36
6:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.607

Line FunctionLemma2.NotAgain!.607:  
----------Proved---------
1:  
     (a18 E {x1|p2(a38) E x1}
      -> *union(a19,*sing(a20)) E {x1|p2(a38) E x1}) & (
     *union(a19,*sing(a20)) E {x1|p2(a38) E x1}
      -> a18 E {x1|p2(a38) E x1})
2:  p2(a38) E a18
3:  <a37,a20> E a36
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a38 E a36
6:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.608

Line FunctionLemma2.NotAgain!.608:  
----------Proved---------
1:  a18 E {x1|p2(a38) E x1}
      -> *union(a19,*sing(a20)) E {x1|p2(a38) E x1}
2:  p2(a38) E a18
3:  <a37,a20> E a36
4:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
5:  a38 E a36
6:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.610, 609

Line FunctionLemma2.NotAgain!.610:  
----------Proved---------
1:  *union(a19,*sing(a20)) E {x1|p2(a38) E x1}
2:  <a37,a20> E a36
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.612

Line FunctionLemma2.NotAgain!.612:  
----------Proved---------
1:  p2(a38) E *union(a19,*sing(a20))
2:  <a37,a20> E a36
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.613

Line FunctionLemma2.NotAgain!.613:  
----------Proved---------
1:  p2(a38) E a19 v p2(a38) E *sing(a20)
2:  <a37,a20> E a36
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!.615, 614

Line FunctionLemma2.NotAgain!.615:  
----------Proved---------
1:  p2(a38) E *sing(a20)
2:  <a37,a20> E a36
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)


|-



 by FunctionLemma2.NotAgain!.616

Line FunctionLemma2.NotAgain!.616:  
----------Proved---------
1:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
2:  a38 E a36
3:  ~a38 E *sing(<a37,a20>)
4:  p2(a38) = a20
5:  <a37,a20> E a36


|-



 by FunctionLemma2.NotAgain!.617

Line FunctionLemma2.NotAgain!.617:  
----------Proved---------
1:  (Ax17.
     <p2(a38),p1(a38)> E *converse(a36) & 
     x17 E *converse(a36) & p2(a38) = p1(x17)
      -> p1(a38) = p2(x17))
2:  a38 E a36
3:  ~a38 E *sing(<a37,a20>)
4:  p2(a38) = a20
5:  <a37,a20> E a36


|-



 by FunctionLemma2.NotAgain!.618

Line FunctionLemma2.NotAgain!.618:  
----------Proved---------
1:  
     <p2(a38),p1(a38)> E *converse(a36) & 
     <a20,a37> E *converse(a36) & p2(a38) = a20
      -> p1(a38) = a37
2:  a38 E a36
3:  ~a38 E *sing(<a37,a20>)
4:  p2(a38) = a20
5:  <a37,a20> E a36


|-



 by FunctionLemma2.NotAgain!.620, 619

Line FunctionLemma2.NotAgain!.620:  
----------Proved---------
1:  ~a38 E *sing(<a37,a20>)
2:  p2(a38) = a20
3:  p1(a38) = a37


|-



 by FunctionLemma2.NotAgain!.627

Line FunctionLemma2.NotAgain!.627:  
----------Proved---------
1:  p2(a38) = a20
2:  p1(a38) = a37


|-

1:  a38 E *sing(<a37,a20>)


 by FunctionLemma2.NotAgain!.628

Line FunctionLemma2.NotAgain!.628:  
----------Proved---------
1:  p2(a38) = a20
2:  p1(a38) = a37


|-

1:  a38 = <a37,a20>


 by FunctionLemma2.NotAgain!.630, 629

Line FunctionLemma2.NotAgain!.630:  
----------Proved---------
1:  p2(a38) = a20


|-

1:  p2(a38) = a20




Line FunctionLemma2.NotAgain!.629:  
----------Proved---------
1:  p1(a38) = a37


|-

1:  p1(a38) = a37




Line FunctionLemma2.NotAgain!.619:  
----------Proved---------
1:  a38 E a36
2:  p2(a38) = a20
3:  <a37,a20> E a36


|-

1:  <p2(a38),p1(a38)> E *converse(a36) & 
     <a20,a37> E *converse(a36) & p2(a38) = a20


 by FunctionLemma2.NotAgain!.622, 621

Line FunctionLemma2.NotAgain!.622:  
----------Proved---------
1:  p2(a38) = a20
2:  <a37,a20> E a36


|-

1:  <a20,a37> E *converse(a36) & p2(a38) = a20


 by FunctionLemma2.NotAgain!.625, 624

Line FunctionLemma2.NotAgain!.625:  
----------Proved---------
1:  p2(a38) = a20


|-

1:  p2(a38) = a20




Line FunctionLemma2.NotAgain!.624:  
----------Proved---------
1:  <a37,a20> E a36


|-

1:  <a20,a37> E *converse(a36)


 by FunctionLemma2.NotAgain!.626

Line FunctionLemma2.NotAgain!.626:  
----------Proved---------
1:  <a37,a20> E a36


|-

1:  <a37,a20> E a36




Line FunctionLemma2.NotAgain!.621:  
----------Proved---------
1:  a38 E a36


|-

1:  <p2(a38),p1(a38)> E *converse(a36)


 by FunctionLemma2.NotAgain!.623

Line FunctionLemma2.NotAgain!.623:  
----------Proved---------
1:  a38 E a36


|-

1:  a38 E a36




Line FunctionLemma2.NotAgain!.614:  
----------Proved---------
1:  p2(a38) E a19


|-

1:  p2(a38) E a19




Line FunctionLemma2.NotAgain!.609:  
----------Proved---------
1:  p2(a38) E a18


|-

1:  a18 E {x1|p2(a38) E x1}


 by FunctionLemma2.NotAgain!.611

Line FunctionLemma2.NotAgain!.611:  
----------Proved---------
1:  p2(a38) E a18


|-

1:  p2(a38) E a18





Proof of lemma FunctionLemma2.NotAgain! ends


Line FunctionLemma2.598:  
----------Proved---------
1:  p2(a38) E a18
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p1(a38) E *imageb(*converse(a36),a19)


 by FunctionLemma2.600

Line FunctionLemma2.600:  
----------Proved---------
1:  p2(a38) E a18
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  (Ex23.x23 E a19 & <x23,p1(a38)> E *converse(a36))


 by FunctionLemma2.601

Line FunctionLemma2.601:  
----------Proved---------
1:  p2(a38) E a18
2:  <a20,a37> E *converse(a36)
3:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
4:  a38 E a36
5:  ~a38 E *sing(<a37,a20>)
6:  a18 = *union(a19,*sing(a20))


|-

1:  p2(a38) E a19 & <p2(a38),p1(a38)> E *converse(a36)


 by FunctionLemma2.603, 602

Line FunctionLemma2.603:  
----------Proved---------
1:  a38 E a36


|-

1:  <p2(a38),p1(a38)> E *converse(a36)


 by FunctionLemma2.631

Line FunctionLemma2.631:  
----------Proved---------
1:  a38 E a36


|-

1:  a38 E a36




Line FunctionLemma2.602:  
----------Proved---------
1:  <a20,a37> E *converse(a36)
2:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))
3:  a38 E a36
4:  ~a38 E *sing(<a37,a20>)
5:  a18 = *union(a19,*sing(a20))
6:  p2(a38) E a18


|-

1:  p2(a38) E a19


 by FunctionLemma2.NotAgain!

Line FunctionLemma2.595:  
----------Proved---------
1:  a38 E a36


|-

1:  a38 E a36





Proof of lemma FunctionLemma2 ends


Line 578:  
----------Proved---------
1:  ~a20 E a19
2:  a18 = *union(a19,*sing(a20))
3:  #function(a21,a18,a36)
4:  <a20,a37> E *converse(a36)
5:  (Ax12.(Ax16.
     x12 E *converse(a36) & x16 E *converse(a36)
      & p1(x12) = p1(x16) -> p2(x12) = p2(x16)))


|-

1:  #function(*imageb(*converse(a36),a19),a19,*setdiff(a36,*sing(<a37,a20>)))


 by FunctionLemma2

Line 552:  
----------Proved---------
1:  a18 = *union(a19,*sing(a20))


|-

1:  a20 E a18


 by 554

Line 554:  
----------Proved---------
1:  (Ax1.a18 E x1 == *union(a19,*sing(a20)) E x1)


|-

1:  a20 E a18


 by 555

Line 555:  
----------Proved---------
1:  a18 E {x1|a20 E x1}
      == *union(a19,*sing(a20)) E {x1|a20 E x1}


|-

1:  a20 E a18


 by 556

Line 556:  
----------Proved---------
1:  
     (a18 E {x1|a20 E x1}
      -> *union(a19,*sing(a20)) E {x1|a20 E x1}) & (
     *union(a19,*sing(a20)) E {x1|a20 E x1}
      -> a18 E {x1|a20 E x1})


|-

1:  a20 E a18


 by 557

Line 557:  
----------Proved---------
1:  *union(a19,*sing(a20)) E {x1|a20 E x1}
      -> a18 E {x1|a20 E x1}


|-

1:  a20 E a18


 by 559, 558

Line 559:  
----------Proved---------
1:  a18 E {x1|a20 E x1}


|-

1:  a20 E a18


 by 564

Line 564:  
----------Proved---------
1:  a20 E a18


|-

1:  a20 E a18




Line 558:  
----------Proved---------


|-

1: