Line 1: ----------Proved--------- |- 1: ~#samesize(*unitset(a1),*powerset(a1)) by 2 Line 2: ----------Proved--------- 1: #samesize(*unitset(a1),*powerset(a1)) |- by 3 Line 3: ----------Proved--------- 1: (Ex5.#function(*unitset(a1),*powerset(a1),x5) & #function(*powerset(a1),*unitset(a1),*converse(x5))) |- by 4 Line 4: ----------Proved--------- 1: #function(*unitset(a1),*powerset(a1),a2) & #function(*powerset(a1),*unitset(a1),*converse(a2)) |- by 5 Line 5: ----------Proved--------- 1: #function(*powerset(a1),*unitset(a1),*converse(a2)) 2: #function(*unitset(a1),*powerset(a1),a2) |- by 6 Line 6: ----------Proved--------- 1: ( #relation(*powerset(a1),*unitset(a1),*converse(a2)) & (Ax7. x7 E *powerset(a1) -> (Ex11. E *converse(a2)))) & (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 2: #function(*unitset(a1),*powerset(a1),a2) |- by 7 Line 7: ----------Proved--------- 1: #relation(*powerset(a1),*unitset(a1),*converse(a2)) & (Ax7. x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 2: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 3: #function(*unitset(a1),*powerset(a1),a2) |- by 8 Line 8: ----------Proved--------- 1: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 2: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 3: #function(*unitset(a1),*powerset(a1),a2) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) |- by 9 Line 9: ----------Proved--------- 1: *temp(a1,a2) E *powerset(a1) -> (Ex18.<*temp(a1,a2),x18> E *converse(a2)) 2: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 3: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 4: #function(*unitset(a1),*powerset(a1),a2) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) |- by 11, 10 Line 11: ----------Proved--------- 1: (Ex18.<*temp(a1,a2),x18> E *converse(a2)) 2: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 3: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 4: #function(*unitset(a1),*powerset(a1),a2) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) |- by 31 Line 31: ----------Proved--------- 1: <*temp(a1,a2),a5> E *converse(a2) 2: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 3: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 4: #function(*unitset(a1),*powerset(a1),a2) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) |- by 32 Line 32: ----------Proved--------- 1: #function(*unitset(a1),*powerset(a1),a2) 2: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 3: E a2 4: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 5: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 33 Line 33: ----------Proved--------- 1: (#relation(*unitset(a1),*powerset(a1),a2) & (Ax56. x56 E *unitset(a1) -> (Ex60. E a2))) & (Ax62.(Ax66. x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 2: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 3: E a2 4: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 5: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 34 Line 34: ----------Proved--------- 1: #relation(*unitset(a1),*powerset(a1),a2) & (Ax56. x56 E *unitset(a1) -> (Ex60. E a2)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 35 Line 35: ----------Proved--------- 1: #relation(*unitset(a1),*powerset(a1),a2) 2: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 36 Line 36: ----------Proved--------- 1: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 2: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 37 Line 37: ----------Proved--------- 1: E a2 -> a5 E *unitset(a1) & *temp(a1,a2) E *powerset(a1) 2: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 3: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 39, 38 Line 39: ----------Proved--------- 1: a5 E *unitset(a1) & *temp(a1,a2) E *powerset(a1) 2: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 3: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 40 Line 40: ----------Proved--------- 1: a5 E *unitset(a1) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 41 Line 41: ----------Proved--------- 1: (Ex75.x75 E a1 & a5 = *sing(x75)) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 42 Line 42: ----------Proved--------- 1: a6 E a1 & a5 = *sing(a6) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- by 43 Line 43: ----------Proved--------- 1: a5 = *sing(a6) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 |- by 44 Line 44: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 |- by 45 Line 45: ----------Proved--------- 1: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} == *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 |- by 46 Line 46: ----------Proved--------- 1: ( a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))}) & ( *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} -> a5 E {x1|(Ex2. E a2 & #includes(x1,x2))}) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 |- by 47 Line 47: ----------Proved--------- 1: *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} -> a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- by 49, 48 Line 49: ----------Proved--------- 1: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 |- by 156, 155 Line 156: ----------Proved--------- 1: *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 |- by 157 Line 157: ----------Proved--------- 1: (Ex125.<*sing(a6),x125> E a2 & #includes(*sing(a6),x125)) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 |- by 158 Line 158: ----------Proved--------- 1: <*sing(a6),a11> E a2 & #includes(*sing(a6),a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 |- by 159 Line 159: ----------Proved--------- 1: #includes(*sing(a6),a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 |- by 160 Line 160: ----------Proved--------- 1: #set(*sing(a6)) & (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 |- by 161 Line 161: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- by 162 Line 162: ----------Proved--------- 1: a6 E *sing(a6) -> a6 E a11 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 4: (Ax76.a5 E x76 == *sing(a6) E x76) 5: *temp(a1,a2) E *powerset(a1) 6: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 7: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 8: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 9: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 10: E a2 11: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 12: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 13: a6 E a1 14: <*sing(a6),a11> E a2 15: #set(*sing(a6)) |- by 164, 163 Line 164: ----------Proved--------- 1: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) |- by 173 Line 173: ----------Proved--------- 1: (Ex131. E a2 & #includes(a5,x131)) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) |- by 174 Line 174: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) |- by 175 Line 175: ----------Proved--------- 1: a5 E {x1| E a2 & #includes(x1,a13)} == *sing(a6) E {x1| E a2 & #includes(x1,a13)} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) 16: E a2 & #includes(a5,a13) |- by 176 Line 176: ----------Proved--------- 1: ( a5 E {x1| E a2 & #includes(x1,a13)} -> *sing(a6) E {x1| E a2 & #includes(x1,a13)}) & ( *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)}) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) 16: E a2 & #includes(a5,a13) |- by 177 Line 177: ----------Proved--------- 1: a5 E {x1| E a2 & #includes(x1,a13)} -> *sing(a6) E {x1| E a2 & #includes(x1,a13)} 2: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) |- by 179, 178 Line 179: ----------Proved--------- 1: *sing(a6) E {x1| E a2 & #includes(x1,a13)} 2: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) |- by 181 Line 181: ----------Proved--------- 1: <*sing(a6),a13> E a2 & #includes(*sing(a6),a13) 2: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) |- by 182 Line 182: ----------Proved--------- 1: #includes(*sing(a6),a13) 2: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) 18: <*sing(a6),a13> E a2 |- by 183 Line 183: ----------Proved--------- 1: #set(*sing(a6)) & (Ax133.x133 E *sing(a6) -> x133 E a13) 2: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) 18: <*sing(a6),a13> E a2 |- by 184 Line 184: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- by 185 Line 185: ----------Proved--------- 1: a5 E {x1| E a2} == *sing(a6) E {x1| E a2} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) 16: E a2 & #includes(a5,a13) 17: <*sing(a6),a13> E a2 18: #set(*sing(a6)) 19: (Ax133.x133 E *sing(a6) -> x133 E a13) 20: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- by 186 Line 186: ----------Proved--------- 1: (a5 E {x1| E a2} -> *sing(a6) E {x1| E a2}) & ( *sing(a6) E {x1| E a2} -> a5 E {x1| E a2}) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) 16: E a2 & #includes(a5,a13) 17: <*sing(a6),a13> E a2 18: #set(*sing(a6)) 19: (Ax133.x133 E *sing(a6) -> x133 E a13) 20: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- by 187 Line 187: ----------Proved--------- 1: a5 E {x1| E a2} -> *sing(a6) E {x1| E a2} 2: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) 18: <*sing(a6),a13> E a2 19: #set(*sing(a6)) 20: (Ax133.x133 E *sing(a6) -> x133 E a13) 21: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- by 189, 188 Line 189: ----------Proved--------- 1: *sing(a6) E {x1| E a2} 2: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) 17: E a2 & #includes(a5,a13) 18: <*sing(a6),a13> E a2 19: #set(*sing(a6)) 20: (Ax133.x133 E *sing(a6) -> x133 E a13) 21: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- by 191 Line 191: ----------Proved--------- 1: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 2: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 3: E a2 4: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 5: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 6: a6 E a1 7: <*sing(a6),a11> E a2 8: #set(*sing(a6)) 9: a6 E a11 10: (Ax127.x127 E *sing(a6) -> x127 E a11) 11: E a2 & #includes(a5,a13) 12: <*sing(a6),a13> E a2 13: #set(*sing(a6)) 14: (Ax133.x133 E *sing(a6) -> x133 E a13) 15: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 16: <*sing(a6),*temp(a1,a2)> E a2 17: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 18: (Ax76.a5 E x76 == *sing(a6) E x76) 19: *temp(a1,a2) E *powerset(a1) 20: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 21: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 192 Line 192: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 193 Line 193: ----------Proved--------- 1: <*sing(a6),*temp(a1,a2)> E a2 & <*sing(a6),a11> E a2 & *sing(a6) = *sing(a6) -> *temp(a1,a2) = a11 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 195, 194 Line 195: ----------Proved--------- 1: *temp(a1,a2) = a11 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 207 Line 207: ----------Proved--------- 1: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 208 Line 208: ----------Proved--------- 1: *temp(a1,a2) E {x1|a6 E x1} == a11 E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 209 Line 209: ----------Proved--------- 1: (*temp(a1,a2) E {x1|a6 E x1} -> a11 E {x1|a6 E x1}) & ( a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1}) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 210 Line 210: ----------Proved--------- 1: *temp(a1,a2) E {x1|a6 E x1} -> a11 E {x1|a6 E x1} 2: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 212, 211 Line 212: ----------Proved--------- 1: a11 E {x1|a6 E x1} 2: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- by 230 Line 230: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a11 |- by 232, 231 Line 232: ----------Proved--------- 1: *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a11 |- by 235 Line 235: ----------Proved--------- 1: a6 E *temp(a1,a2) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a11 |- by 236 Line 236: ----------Proved--------- 1: a6 E a1 & (Ax157.<*sing(a6),x157> E a2 -> ~a6 E x157) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a11 |- by 237 Line 237: ----------Proved--------- 1: (Ax157.<*sing(a6),x157> E a2 -> ~a6 E x157) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a11 26: a6 E a1 |- by 238 Line 238: ----------Proved--------- 1: <*sing(a6),a11> E a2 -> ~a6 E a11 2: (Ax157.<*sing(a6),x157> E a2 -> ~a6 E x157) 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 26: a6 E a11 27: a6 E a1 |- by 240, 239 Line 240: ----------Proved--------- 1: ~a6 E a11 2: (Ax157.<*sing(a6),x157> E a2 -> ~a6 E x157) 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 26: a6 E a11 27: a6 E a1 |- by 241 Line 241: ----------Proved--------- 1: a6 E a11 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: E a2 & #includes(a5,a13) 4: <*sing(a6),a13> E a2 5: #set(*sing(a6)) 6: (Ax133.x133 E *sing(a6) -> x133 E a13) 7: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 8: <*sing(a6),*temp(a1,a2)> E a2 9: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 10: (Ax76.a5 E x76 == *sing(a6) E x76) 11: *temp(a1,a2) E *powerset(a1) 12: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 13: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 14: a6 E a11 15: a6 E a1 16: (Ax157.<*sing(a6),x157> E a2 -> ~a6 E x157) 17: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 18: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 19: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 20: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 21: E a2 22: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 23: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 24: a6 E a1 25: <*sing(a6),a11> E a2 26: #set(*sing(a6)) |- 1: a6 E a11 Line 239: ----------Proved--------- 1: <*sing(a6),a11> E a2 2: #set(*sing(a6)) 3: a6 E a11 4: (Ax127.x127 E *sing(a6) -> x127 E a11) 5: E a2 & #includes(a5,a13) 6: <*sing(a6),a13> E a2 7: #set(*sing(a6)) 8: (Ax133.x133 E *sing(a6) -> x133 E a13) 9: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 10: <*sing(a6),*temp(a1,a2)> E a2 11: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 12: (Ax76.a5 E x76 == *sing(a6) E x76) 13: *temp(a1,a2) E *powerset(a1) 14: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 15: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 16: a6 E a11 17: a6 E a1 18: (Ax157.<*sing(a6),x157> E a2 -> ~a6 E x157) 19: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 20: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 21: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 22: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 23: E a2 24: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 25: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 26: a6 E a1 |- 1: <*sing(a6),a11> E a2 Line 231: ----------Proved--------- 1: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 24: a6 E a11 |- 1: a11 E {x1|a6 E x1} by 233 Line 233: ----------Proved--------- 1: *temp(a1,a2) E {x1|a6 E x1} == a11 E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a11 |- 1: a11 E {x1|a6 E x1} by 234 Line 234: ----------Proved--------- 1: a6 E a11 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: E a2 & #includes(a5,a13) 4: <*sing(a6),a13> E a2 5: #set(*sing(a6)) 6: (Ax133.x133 E *sing(a6) -> x133 E a13) 7: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 8: <*sing(a6),*temp(a1,a2)> E a2 9: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 10: (Ax76.a5 E x76 == *sing(a6) E x76) 11: *temp(a1,a2) E *powerset(a1) 12: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 13: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 14: a6 E a11 15: *temp(a1,a2) E {x1|a6 E x1} == a11 E {x1|a6 E x1} 16: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 17: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 18: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 19: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 20: E a2 21: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 22: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 23: a6 E a1 24: <*sing(a6),a11> E a2 25: #set(*sing(a6)) |- 1: a6 E a11 Line 211: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *temp(a1,a2) E {x1|a6 E x1} by 213 Line 213: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: a6 E *temp(a1,a2) by 214 Line 214: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: a6 E a1 & (Ax143.<*sing(a6),x143> E a2 -> ~a6 E x143) by 216, 215 Line 216: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: (Ax143.<*sing(a6),x143> E a2 -> ~a6 E x143) by 217 Line 217: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: <*sing(a6),a15> E a2 -> ~a6 E a15 by 218 Line 218: ----------Proved--------- 1: <*sing(a6),a15> E a2 2: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: ~a6 E a15 by 219 Line 219: ----------Proved--------- 1: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a15 26: <*sing(a6),a15> E a2 |- by 221, 220 Line 221: ----------Proved--------- 1: *temp(a1,a2) E {x1|a6 E x1} 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a15 26: <*sing(a6),a15> E a2 |- by 223 Line 223: ----------Proved--------- 1: a6 E *temp(a1,a2) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a15 26: <*sing(a6),a15> E a2 |- by 224 Line 224: ----------Proved--------- 1: a6 E a1 & (Ax150.<*sing(a6),x150> E a2 -> ~a6 E x150) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a15 26: <*sing(a6),a15> E a2 |- by 225 Line 225: ----------Proved--------- 1: (Ax150.<*sing(a6),x150> E a2 -> ~a6 E x150) 2: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 3: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 4: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 5: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 6: E a2 7: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 8: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 9: a6 E a1 10: <*sing(a6),a11> E a2 11: #set(*sing(a6)) 12: a6 E a11 13: (Ax127.x127 E *sing(a6) -> x127 E a11) 14: E a2 & #includes(a5,a13) 15: <*sing(a6),a13> E a2 16: #set(*sing(a6)) 17: (Ax133.x133 E *sing(a6) -> x133 E a13) 18: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 19: <*sing(a6),*temp(a1,a2)> E a2 20: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 21: (Ax76.a5 E x76 == *sing(a6) E x76) 22: *temp(a1,a2) E *powerset(a1) 23: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 24: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 25: a6 E a15 26: <*sing(a6),a15> E a2 27: a6 E a1 |- by 226 Line 226: ----------Proved--------- 1: <*sing(a6),a11> E a2 -> ~a6 E a11 2: (Ax150.<*sing(a6),x150> E a2 -> ~a6 E x150) 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 26: a6 E a15 27: <*sing(a6),a15> E a2 28: a6 E a1 |- by 228, 227 Line 228: ----------Proved--------- 1: ~a6 E a11 2: (Ax150.<*sing(a6),x150> E a2 -> ~a6 E x150) 3: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 4: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: <*sing(a6),a11> E a2 12: #set(*sing(a6)) 13: a6 E a11 14: (Ax127.x127 E *sing(a6) -> x127 E a11) 15: E a2 & #includes(a5,a13) 16: <*sing(a6),a13> E a2 17: #set(*sing(a6)) 18: (Ax133.x133 E *sing(a6) -> x133 E a13) 19: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 20: <*sing(a6),*temp(a1,a2)> E a2 21: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 22: (Ax76.a5 E x76 == *sing(a6) E x76) 23: *temp(a1,a2) E *powerset(a1) 24: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 25: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 26: a6 E a15 27: <*sing(a6),a15> E a2 28: a6 E a1 |- by 229 Line 229: ----------Proved--------- 1: a6 E a11 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: E a2 & #includes(a5,a13) 4: <*sing(a6),a13> E a2 5: #set(*sing(a6)) 6: (Ax133.x133 E *sing(a6) -> x133 E a13) 7: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 8: <*sing(a6),*temp(a1,a2)> E a2 9: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 10: (Ax76.a5 E x76 == *sing(a6) E x76) 11: *temp(a1,a2) E *powerset(a1) 12: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 13: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 14: a6 E a15 15: <*sing(a6),a15> E a2 16: a6 E a1 17: (Ax150.<*sing(a6),x150> E a2 -> ~a6 E x150) 18: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 19: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 20: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 21: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 22: E a2 23: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 24: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 25: a6 E a1 26: <*sing(a6),a11> E a2 27: #set(*sing(a6)) |- 1: a6 E a11 Line 227: ----------Proved--------- 1: <*sing(a6),a11> E a2 2: #set(*sing(a6)) 3: a6 E a11 4: (Ax127.x127 E *sing(a6) -> x127 E a11) 5: E a2 & #includes(a5,a13) 6: <*sing(a6),a13> E a2 7: #set(*sing(a6)) 8: (Ax133.x133 E *sing(a6) -> x133 E a13) 9: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 10: <*sing(a6),*temp(a1,a2)> E a2 11: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 12: (Ax76.a5 E x76 == *sing(a6) E x76) 13: *temp(a1,a2) E *powerset(a1) 14: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 15: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 16: a6 E a15 17: <*sing(a6),a15> E a2 18: a6 E a1 19: (Ax150.<*sing(a6),x150> E a2 -> ~a6 E x150) 20: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 21: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 22: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 23: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 24: E a2 25: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 26: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 27: a6 E a1 |- 1: <*sing(a6),a11> E a2 Line 220: ----------Proved--------- 1: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 24: a6 E a15 25: <*sing(a6),a15> E a2 |- 1: a11 E {x1|a6 E x1} by 222 Line 222: ----------Proved--------- 1: a6 E a11 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: E a2 & #includes(a5,a13) 4: <*sing(a6),a13> E a2 5: #set(*sing(a6)) 6: (Ax133.x133 E *sing(a6) -> x133 E a13) 7: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 8: <*sing(a6),*temp(a1,a2)> E a2 9: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 10: (Ax76.a5 E x76 == *sing(a6) E x76) 11: *temp(a1,a2) E *powerset(a1) 12: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 13: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 14: a6 E a15 15: <*sing(a6),a15> E a2 16: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 17: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 18: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 19: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 20: E a2 21: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 22: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 23: a6 E a1 24: <*sing(a6),a11> E a2 25: #set(*sing(a6)) |- 1: a6 E a11 Line 215: ----------Proved--------- 1: a6 E a1 2: <*sing(a6),a11> E a2 3: #set(*sing(a6)) 4: a6 E a11 5: (Ax127.x127 E *sing(a6) -> x127 E a11) 6: E a2 & #includes(a5,a13) 7: <*sing(a6),a13> E a2 8: #set(*sing(a6)) 9: (Ax133.x133 E *sing(a6) -> x133 E a13) 10: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 11: <*sing(a6),*temp(a1,a2)> E a2 12: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 13: (Ax76.a5 E x76 == *sing(a6) E x76) 14: *temp(a1,a2) E *powerset(a1) 15: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 16: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 17: a11 E {x1|a6 E x1} -> *temp(a1,a2) E {x1|a6 E x1} 18: (Ax136.*temp(a1,a2) E x136 == a11 E x136) 19: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 20: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 21: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 22: E a2 23: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 24: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) |- 1: a6 E a1 Line 194: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: <*sing(a6),*temp(a1,a2)> E a2 & <*sing(a6),a11> E a2 & *sing(a6) = *sing(a6) by 197, 196 Line 197: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: <*sing(a6),a11> E a2 & *sing(a6) = *sing(a6) by 199, 198 Line 199: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *sing(a6) = *sing(a6) by 200 Line 200: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: (Ax135.*sing(a6) E x135 == *sing(a6) E x135) 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) by 201 Line 201: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *sing(a6) E a14 == *sing(a6) E a14 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) by 202 Line 202: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: (*sing(a6) E a14 -> *sing(a6) E a14) & ( *sing(a6) E a14 -> *sing(a6) E a14) 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) by 204, 203 Line 204: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *sing(a6) E a14 -> *sing(a6) E a14 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) by 206 Line 206: ----------Proved--------- 1: *sing(a6) E a14 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *sing(a6) E a14 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) Line 203: ----------Proved--------- 1: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 2: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 3: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 4: E a2 5: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 6: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 7: a6 E a1 8: <*sing(a6),a11> E a2 9: #set(*sing(a6)) 10: a6 E a11 11: (Ax127.x127 E *sing(a6) -> x127 E a11) 12: E a2 & #includes(a5,a13) 13: <*sing(a6),a13> E a2 14: #set(*sing(a6)) 15: (Ax133.x133 E *sing(a6) -> x133 E a13) 16: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 17: <*sing(a6),*temp(a1,a2)> E a2 18: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 19: (Ax76.a5 E x76 == *sing(a6) E x76) 20: *temp(a1,a2) E *powerset(a1) 21: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 22: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *sing(a6) E a14 -> *sing(a6) E a14 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) by 205 Line 205: ----------Proved--------- 1: *sing(a6) E a14 2: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 3: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 4: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 5: E a2 6: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 7: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 8: a6 E a1 9: <*sing(a6),a11> E a2 10: #set(*sing(a6)) 11: a6 E a11 12: (Ax127.x127 E *sing(a6) -> x127 E a11) 13: E a2 & #includes(a5,a13) 14: <*sing(a6),a13> E a2 15: #set(*sing(a6)) 16: (Ax133.x133 E *sing(a6) -> x133 E a13) 17: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 18: <*sing(a6),*temp(a1,a2)> E a2 19: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 20: (Ax76.a5 E x76 == *sing(a6) E x76) 21: *temp(a1,a2) E *powerset(a1) 22: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 23: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) |- 1: *sing(a6) E a14 2: (Ex135.x135 E *sing(a6) v x135 E *sing(a6)) & (Ax135. x135 E *sing(a6) == x135 E *sing(a6)) Line 198: ----------Proved--------- 1: <*sing(a6),a11> E a2 2: #set(*sing(a6)) 3: a6 E a11 4: (Ax127.x127 E *sing(a6) -> x127 E a11) 5: E a2 & #includes(a5,a13) 6: <*sing(a6),a13> E a2 7: #set(*sing(a6)) 8: (Ax133.x133 E *sing(a6) -> x133 E a13) 9: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 10: <*sing(a6),*temp(a1,a2)> E a2 11: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 12: (Ax76.a5 E x76 == *sing(a6) E x76) 13: *temp(a1,a2) E *powerset(a1) 14: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 15: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 16: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 17: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 18: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 19: E a2 20: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 21: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 22: a6 E a1 |- 1: <*sing(a6),a11> E a2 Line 196: ----------Proved--------- 1: <*sing(a6),*temp(a1,a2)> E a2 2: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax134. <*sing(a6),*temp(a1,a2)> E a2 & x134 E a2 & *sing(a6) = p1(x134) -> *temp(a1,a2) = p2(x134)) 8: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 9: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 10: E a2 11: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 12: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 13: a6 E a1 14: <*sing(a6),a11> E a2 15: #set(*sing(a6)) 16: a6 E a11 17: (Ax127.x127 E *sing(a6) -> x127 E a11) 18: E a2 & #includes(a5,a13) 19: <*sing(a6),a13> E a2 20: #set(*sing(a6)) 21: (Ax133.x133 E *sing(a6) -> x133 E a13) 22: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- 1: <*sing(a6),*temp(a1,a2)> E a2 Line 188: ----------Proved--------- 1: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) 16: E a2 & #includes(a5,a13) 17: <*sing(a6),a13> E a2 18: #set(*sing(a6)) 19: (Ax133.x133 E *sing(a6) -> x133 E a13) 20: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} |- 1: a5 E {x1| E a2} by 190 Line 190: ----------Proved--------- 1: E a2 2: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 3: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 4: a6 E a1 5: <*sing(a6),a11> E a2 6: #set(*sing(a6)) 7: a6 E a11 8: (Ax127.x127 E *sing(a6) -> x127 E a11) 9: E a2 & #includes(a5,a13) 10: <*sing(a6),a13> E a2 11: #set(*sing(a6)) 12: (Ax133.x133 E *sing(a6) -> x133 E a13) 13: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 14: *sing(a6) E {x1| E a2} -> a5 E {x1| E a2} 15: (Ax76.a5 E x76 == *sing(a6) E x76) 16: *temp(a1,a2) E *powerset(a1) 17: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 18: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 19: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 20: #relation(*powerset(a1),*unitset(a1),*converse(a2)) |- 1: E a2 Line 178: ----------Proved--------- 1: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: <*sing(a6),a11> E a2 13: #set(*sing(a6)) 14: a6 E a11 15: (Ax127.x127 E *sing(a6) -> x127 E a11) 16: E a2 & #includes(a5,a13) |- 1: a5 E {x1| E a2 & #includes(x1,a13)} by 180 Line 180: ----------Proved--------- 1: E a2 & #includes(a5,a13) 2: *sing(a6) E {x1| E a2 & #includes(x1,a13)} -> a5 E {x1| E a2 & #includes(x1,a13)} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) 15: a6 E a11 16: (Ax127.x127 E *sing(a6) -> x127 E a11) |- 1: E a2 & #includes(a5,a13) Line 163: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: a6 E *sing(a6) by 165 Line 165: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: a6 = a6 by 166 Line 166: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: (Ax130.a6 E x130 == a6 E x130) 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) by 167 Line 167: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: a6 E a12 == a6 E a12 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) by 168 Line 168: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: (a6 E a12 -> a6 E a12) & (a6 E a12 -> a6 E a12) 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) by 170, 169 Line 170: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: a6 E a12 -> a6 E a12 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) by 172 Line 172: ----------Proved--------- 1: a6 E a12 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 4: (Ax76.a5 E x76 == *sing(a6) E x76) 5: *temp(a1,a2) E *powerset(a1) 6: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 7: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 8: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 9: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 10: E a2 11: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 12: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 13: a6 E a1 14: <*sing(a6),a11> E a2 15: #set(*sing(a6)) |- 1: a6 E a12 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) Line 169: ----------Proved--------- 1: (Ax127.x127 E *sing(a6) -> x127 E a11) 2: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: <*sing(a6),a11> E a2 14: #set(*sing(a6)) |- 1: a6 E a12 -> a6 E a12 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) by 171 Line 171: ----------Proved--------- 1: a6 E a12 2: (Ax127.x127 E *sing(a6) -> x127 E a11) 3: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 4: (Ax76.a5 E x76 == *sing(a6) E x76) 5: *temp(a1,a2) E *powerset(a1) 6: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 7: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 8: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 9: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 10: E a2 11: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 12: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 13: a6 E a1 14: <*sing(a6),a11> E a2 15: #set(*sing(a6)) |- 1: a6 E a12 2: (Ex130.x130 E a6 v x130 E a6) & (Ax130. x130 E a6 == x130 E a6) Line 155: ----------Proved--------- 1: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 |- 1: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} Line 48: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} by 50 Line 50: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 51 Line 51: ----------Proved--------- 1: a5 E *temp(a1,a2) == *sing(a6) E *temp(a1,a2) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 52 Line 52: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: <*sing(a6),*temp(a1,a2)> E a2 & #includes(*sing(a6),*temp(a1,a2)) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 54, 53 Line 54: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: #includes(*sing(a6),*temp(a1,a2)) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 62 Line 62: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: #set(*sing(a6)) & (Ax79.x79 E *sing(a6) -> x79 E *temp(a1,a2)) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 64, 63 Line 64: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: (Ax79.x79 E *sing(a6) -> x79 E *temp(a1,a2)) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 76 Line 76: ----------Proved--------- 1: (Ax76.a5 E x76 == *sing(a6) E x76) 2: *temp(a1,a2) E *powerset(a1) 3: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 4: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 5: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 6: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 7: E a2 8: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 9: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 10: a6 E a1 11: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: a8 E *sing(a6) -> a8 E *temp(a1,a2) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 77 Line 77: ----------Proved--------- 1: a8 E *sing(a6) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: a8 E *temp(a1,a2) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 78 Line 78: ----------Proved--------- 1: a8 E *sing(a6) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: a8 E a1 & (Ax94.<*sing(a8),x94> E a2 -> ~a8 E x94) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 80, 79 Line 80: ----------Proved--------- 1: a8 E *sing(a6) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: (Ax94.<*sing(a8),x94> E a2 -> ~a8 E x94) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 92 Line 92: ----------Proved--------- 1: a8 = a6 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: (Ax94.<*sing(a8),x94> E a2 -> ~a8 E x94) 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 93 Line 93: ----------Proved--------- 1: a8 = a6 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: <*sing(a8),a9> E a2 -> ~a8 E a9 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 94 Line 94: ----------Proved--------- 1: <*sing(a8),a9> E a2 2: a8 = a6 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} |- 1: ~a8 E a9 2: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 95 Line 95: ----------Proved--------- 1: a8 = a6 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 13: a8 E a9 14: <*sing(a8),a9> E a2 |- 1: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 96 Line 96: ----------Proved--------- 1: (Ax100.a8 E x100 == a6 E x100) 2: (Ax76.a5 E x76 == *sing(a6) E x76) 3: *temp(a1,a2) E *powerset(a1) 4: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 5: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 6: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 7: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 8: E a2 9: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 10: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 11: a6 E a1 12: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 13: a8 E a9 14: <*sing(a8),a9> E a2 |- 1: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 97 Line 97: ----------Proved--------- 1: a8 E {x1|<*sing(x1),a9> E a2} == a6 E {x1|<*sing(x1),a9> E a2} 2: (Ax100.a8 E x100 == a6 E x100) 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 14: a8 E a9 15: <*sing(a8),a9> E a2 |- 1: (Ex77.<*sing(a6),x77> E a2 & #includes(*sing(a6),x77)) by 98 Line 98: ----------Proved--------- 1: (a8 E {x1|<*sing(x1),a9> E a2} -> a6 E {x1|<*sing(x1),a9> E a2}) & ( a6 E {x1|<*sing(x1),a9> E a2} -> a8 E {x1|<*sing(x1),a9> E a2}) 2: (Ax100.a8 E x100 == a6 E x100) 3: (Ax76.a5 E x76 == *sing(a6) E x76) 4: *temp(a1,a2) E *powerset(a1) 5: (Ax68.x68 E a2 -> p1(x68) E *unitset(a1) & p2(x68) E *powerset(a1)) 6: (Ax56.x56 E *unitset(a1) -> (Ex60. E a2)) 7: (Ax62.(Ax66.x62 E a2 & x66 E a2 & p1(x62) = p1(x66) -> p2(x62) = p2(x66))) 8: #relation(*powerset(a1),*unitset(a1),*converse(a2)) 9: E a2 10: (Ax7.x7 E *powerset(a1) -> (Ex11. E *converse(a2))) 11: (Ax13.(Ax17. x13 E *converse(a2) & x17 E *converse(a2) & p1(x13) = p1(x17) -> p2(x13) = p2(x17))) 12: a6 E a1 13: a5 E {x1|(Ex2. E a2 & #includes(x1,x2))} -> *sing(a6) E {x1|(Ex2. E a2 & #includes(x1,x2))} 14: a8 E a9 15: <*sing(a8),a9> E a2 |- 1: (Ex77.<*sing(a6),x77> E a2 & #inc