%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET641+3 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 05:43:05 EDT 2022 % Result : Theorem 27.08s 27.29s % Output : Proof 27.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET641+3 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jul 10 08:23:43 EDT 2022 % 0.13/0.34 % CPUTime : % 27.08/27.29 % SZS status Theorem % 27.08/27.29 (* PROOF-FOUND *) % 27.08/27.29 (* BEGIN-PROOF *) % 27.08/27.29 % SZS output start Proof % 27.08/27.29 1. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 27.08/27.29 2. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 27.08/27.29 3. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 27.08/27.29 4. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 27.08/27.29 5. (-. (ilf_type (cross_product T_0 T_1) (set_type))) (ilf_type (cross_product T_0 T_1) (set_type)) ### Axiom % 27.08/27.29 6. ((ilf_type T_1 (set_type)) => (ilf_type (cross_product T_0 T_1) (set_type))) (-. (ilf_type (cross_product T_0 T_1) (set_type))) (ilf_type T_1 (set_type)) ### Imply 4 5 % 27.08/27.29 7. (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product T_0 C) (set_type)))) (ilf_type T_1 (set_type)) (-. (ilf_type (cross_product T_0 T_1) (set_type))) ### All 6 % 27.08/27.29 8. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product T_0 C) (set_type))))) (-. (ilf_type (cross_product T_0 T_1) (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) ### Imply 3 7 % 27.08/27.29 9. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (cross_product T_0 T_1) (set_type))) ### All 8 % 27.08/27.29 10. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 27.08/27.29 11. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 27.08/27.29 12. (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (ilf_type (power_set (cross_product T_0 T_1)) (set_type)) ### Axiom % 27.08/27.29 13. ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) ### And 12 % 27.08/27.29 14. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type)))) (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 13 % 27.08/27.29 15. (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) ### All 14 % 27.08/27.29 16. (-. (empty (power_set (cross_product T_0 T_1)))) (empty (power_set (cross_product T_0 T_1))) ### Axiom % 27.08/27.29 17. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 27.08/27.29 18. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 27.08/27.29 19. (subset T_2 (cross_product T_0 T_1)) (-. (subset T_2 (cross_product T_0 T_1))) ### Axiom % 27.08/27.29 20. (-. (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1))))) ### Axiom % 27.08/27.29 21. ((subset T_2 (cross_product T_0 T_1)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (-. (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (subset T_2 (cross_product T_0 T_1)) ### Equiv 19 20 % 27.08/27.29 22. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((subset T_2 (cross_product T_0 T_1)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1))))))) (subset T_2 (cross_product T_0 T_1)) (-. (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 21 % 27.08/27.29 23. (All C, ((ilf_type C (set_type)) => ((subset T_2 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D C))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (subset T_2 (cross_product T_0 T_1)) ### All 22 % 27.08/27.29 24. ((ilf_type T_2 (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset T_2 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D C)))))))) (subset T_2 (cross_product T_0 T_1)) (-. (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) ### Imply 18 23 % 27.08/27.29 25. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (subset T_2 (cross_product T_0 T_1)) ### All 24 % 27.08/27.29 26. (-. (member T_2 (power_set (cross_product T_0 T_1)))) (member T_2 (power_set (cross_product T_0 T_1))) ### Axiom % 27.08/27.29 27. ((member T_2 (power_set (cross_product T_0 T_1))) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1)))))) (-. (member T_2 (power_set (cross_product T_0 T_1)))) (subset T_2 (cross_product T_0 T_1)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### Equiv 25 26 % 27.08/27.29 28. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((member T_2 (power_set (cross_product T_0 T_1))) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D (cross_product T_0 T_1))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (subset T_2 (cross_product T_0 T_1)) (-. (member T_2 (power_set (cross_product T_0 T_1)))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 27 % 27.08/27.29 29. (All C, ((ilf_type C (set_type)) => ((member T_2 (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D C))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (member T_2 (power_set (cross_product T_0 T_1)))) (subset T_2 (cross_product T_0 T_1)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### All 28 % 27.08/27.29 30. ((ilf_type T_2 (set_type)) => (All C, ((ilf_type C (set_type)) => ((member T_2 (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_2) => (member D C)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (-. (member T_2 (power_set (cross_product T_0 T_1)))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) ### Imply 17 29 % 27.08/27.29 31. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (member T_2 (power_set (cross_product T_0 T_1)))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### All 30 % 27.15/27.33 32. (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1)))) ### Axiom % 27.15/27.33 33. ((ilf_type T_2 (member_type (power_set (cross_product T_0 T_1)))) <=> (member T_2 (power_set (cross_product T_0 T_1)))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### Equiv 31 32 % 27.15/27.33 34. (((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) => ((ilf_type T_2 (member_type (power_set (cross_product T_0 T_1)))) <=> (member T_2 (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (-. (empty (power_set (cross_product T_0 T_1)))) ### DisjTree 16 15 33 % 27.15/27.33 35. (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type T_2 (member_type C)) <=> (member T_2 C)))) (-. (empty (power_set (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### All 34 % 27.15/27.33 36. (empty (power_set (cross_product T_0 T_1))) (-. (empty (power_set (cross_product T_0 T_1)))) ### Axiom % 27.15/27.33 37. ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (empty (power_set (cross_product T_0 T_1))) ### And 36 % 27.15/27.33 38. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type)))) (empty (power_set (cross_product T_0 T_1))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 37 % 27.15/27.33 39. (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (empty (power_set (cross_product T_0 T_1))) ### All 38 % 27.15/27.33 40. ((empty (power_set (cross_product T_0 T_1))) <=> (All C, ((ilf_type C (set_type)) => (-. (member C (power_set (cross_product T_0 T_1))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type T_2 (member_type C)) <=> (member T_2 C)))) ### Equiv 35 39 % 27.15/27.33 41. ((ilf_type (power_set (cross_product T_0 T_1)) (set_type)) => ((empty (power_set (cross_product T_0 T_1))) <=> (All C, ((ilf_type C (set_type)) => (-. (member C (power_set (cross_product T_0 T_1)))))))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type T_2 (member_type C)) <=> (member T_2 C)))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) ### Imply 15 40 % 27.15/27.33 42. (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type T_2 (member_type C)) <=> (member T_2 C)))) ### All 41 % 27.15/27.33 43. ((ilf_type T_2 (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type T_2 (member_type C)) <=> (member T_2 C))))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (ilf_type T_2 (set_type)) ### Imply 11 42 % 27.40/27.58 44. (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) ### All 43 % 27.40/27.58 45. (-. (ilf_type T_2 (subset_type (cross_product T_0 T_1)))) (ilf_type T_2 (subset_type (cross_product T_0 T_1))) ### Axiom % 27.40/27.58 46. ((ilf_type T_2 (subset_type (cross_product T_0 T_1))) <=> (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1))))) (-. (ilf_type T_2 (subset_type (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) ### Equiv 44 45 % 27.40/27.58 47. ((ilf_type T_2 (set_type)) => ((ilf_type T_2 (subset_type (cross_product T_0 T_1))) <=> (ilf_type T_2 (member_type (power_set (cross_product T_0 T_1)))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type T_2 (subset_type (cross_product T_0 T_1)))) (ilf_type T_2 (set_type)) ### Imply 10 46 % 27.40/27.58 48. (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type (cross_product T_0 T_1))) <=> (ilf_type C (member_type (power_set (cross_product T_0 T_1))))))) (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (subset_type (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) ### All 47 % 27.40/27.58 49. ((ilf_type (cross_product T_0 T_1) (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type (cross_product T_0 T_1))) <=> (ilf_type C (member_type (power_set (cross_product T_0 T_1)))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type T_2 (subset_type (cross_product T_0 T_1)))) (ilf_type T_2 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 48 % 27.40/27.58 50. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (subset_type (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) ### All 49 % 27.40/27.58 51. (-. (ilf_type T_2 (relation_type T_0 T_1))) (ilf_type T_2 (relation_type T_0 T_1)) ### Axiom % 27.40/27.58 52. ((ilf_type T_2 (subset_type (cross_product T_0 T_1))) => (ilf_type T_2 (relation_type T_0 T_1))) (-. (ilf_type T_2 (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### Imply 50 51 % 27.40/27.60 53. (All D, ((ilf_type D (subset_type (cross_product T_0 T_1))) => (ilf_type D (relation_type T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (-. (ilf_type T_2 (relation_type T_0 T_1))) ### All 52 % 27.40/27.60 54. ((All D, ((ilf_type D (subset_type (cross_product T_0 T_1))) => (ilf_type D (relation_type T_0 T_1)))) /\ (All E, ((ilf_type E (relation_type T_0 T_1)) => (ilf_type E (subset_type (cross_product T_0 T_1)))))) (-. (ilf_type T_2 (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### And 53 % 27.40/27.60 55. ((ilf_type T_1 (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product T_0 T_1))) => (ilf_type D (relation_type T_0 T_1)))) /\ (All E, ((ilf_type E (relation_type T_0 T_1)) => (ilf_type E (subset_type (cross_product T_0 T_1))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (-. (ilf_type T_2 (relation_type T_0 T_1))) (ilf_type T_1 (set_type)) ### Imply 2 54 % 27.40/27.60 56. (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product T_0 C))) => (ilf_type D (relation_type T_0 C)))) /\ (All E, ((ilf_type E (relation_type T_0 C)) => (ilf_type E (subset_type (cross_product T_0 C)))))))) (ilf_type T_1 (set_type)) (-. (ilf_type T_2 (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### All 55 % 27.40/27.60 57. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product T_0 C))) => (ilf_type D (relation_type T_0 C)))) /\ (All E, ((ilf_type E (relation_type T_0 C)) => (ilf_type E (subset_type (cross_product T_0 C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (-. (ilf_type T_2 (relation_type T_0 T_1))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) ### Imply 1 56 % 27.40/27.60 58. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type T_2 (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_2 (cross_product T_0 T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### All 57 % 27.40/27.60 59. (-. ((ilf_type T_1 (set_type)) => ((subset T_2 (cross_product T_0 T_1)) => (ilf_type T_2 (relation_type T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) ### ConjTree 58 % 27.40/27.61 60. (-. (All D, ((ilf_type D (set_type)) => ((subset T_2 (cross_product T_0 D)) => (ilf_type T_2 (relation_type T_0 D)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### NotAllEx 59 % 27.40/27.61 61. (-. ((ilf_type T_0 (set_type)) => (All D, ((ilf_type D (set_type)) => ((subset T_2 (cross_product T_0 D)) => (ilf_type T_2 (relation_type T_0 D))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) ### NotImply 60 % 27.40/27.61 62. (-. (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => ((subset T_2 (cross_product C D)) => (ilf_type T_2 (relation_type C D)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### NotAllEx 61 % 27.40/27.61 63. (-. ((ilf_type T_2 (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => ((subset T_2 (cross_product C D)) => (ilf_type T_2 (relation_type C D))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) ### NotImply 62 % 27.40/27.61 64. (-. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => ((subset B (cross_product C D)) => (ilf_type B (relation_type C D)))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### NotAllEx 63 % 27.40/27.61 % SZS output end Proof % 27.40/27.61 (* END-PROOF *) %------------------------------------------------------------------------------