| pf |
|---|
Let x0 of type ι be given.
Assume H5: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2). Apply unknownprop_500d1e737e2209e4c583d05afc878803ba55ca9b82cd3357b41edde686af0c3b with u3, x0, False leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying H1.
The subproof is completed by applying L6.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H8: x2 ∈ x0.
Assume H9: x1 ⊆ x0.
Assume H10: x1 ⊆ x2.
Apply unknownprop_9c3c4976195baf6bd37497317b74ca268d712dfbd75862a7bcb0572a39ded839 with u2, x1, False leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying H7.
Let x3 of type ι be given.
Assume H13: x3 ∈ x1.
Apply L6 with x3.
Apply H9 with x3.
The subproof is completed by applying H13.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H14: x4 ∈ x1.
Assume H15: x3 ⊆ x1.
Assume H16: x3 ⊆ x4.
Apply unknownprop_40f47bd5727e3c8306e109a25c685ee358c3452e21455ab7ec4201d838abbfbf with x2, λ x5 . x2 = x5 ⟶ ∀ x6 : ο . x6 leaving 7 subgoals.
Apply setminusI with u11, u6, x2 leaving 2 subgoals.
Apply H0 with x2.
The subproof is completed by applying H8.
Apply unknownprop_484eb1f2b1000075d76e9baee6b85ab01e63797b5b963f20f71e7fa99b2108e3 with binunion x1 (Sing x2) leaving 3 subgoals.
Let x5 of type ι be given.
Apply binunionE with x1, Sing x2, x5, x5 ∈ u6 leaving 3 subgoals.
The subproof is completed by applying H21.
Assume H22: x5 ∈ x1.
Apply nat_trans with u6, x2, x5 leaving 3 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying H20.
Apply H10 with x5.
The subproof is completed by applying H22.
Assume H22: x5 ∈ Sing x2. Apply SingE with x2, x5, λ x6 x7 . x7 ∈ u6 leaving 2 subgoals.
The subproof is completed by applying H22.
The subproof is completed by applying H20.
Apply equip_atleastp with u4, binunion x1 (Sing x2).
Apply equip_tra with u4, setsum x1 (Sing x2), binunion x1 (Sing x2) leaving 2 subgoals.
Apply unknownprop_3d49cae020bbbfc37618d229c52b061e89851b6bf6d51c1368f17fc973c0456f with λ x5 x6 . equip x5 (setsum x1 (Sing x2)).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with u3, u1, x1, Sing x2 leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying nat_1.
The subproof is completed by applying H7.
Apply equip_sym with Sing x2, u1.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x2.
Apply equip_sym with binunion x1 (Sing x2), setsum x1 (Sing x2).
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with x1, Sing x2, x1, Sing x2 leaving 3 subgoals.
The subproof is completed by applying equip_ref with x1.
The subproof is completed by applying equip_ref with Sing x2. Let x5 of type ι be given.
Assume H21: x5 ∈ x1.
Assume H22: x5 ∈ Sing x2. Apply In_irref with x2.
Apply SingE with x2, x5, λ x6 x7 . x6 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H22.
Apply H10 with x5.
The subproof is completed by applying H21.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply H5 with x5, x6 leaving 2 subgoals.
Apply L11 with x5.
The subproof is completed by applying H21.
Apply L11 with x6.
The subproof is completed by applying H22.
Apply L12.
Apply Subq_tra with x1, x2, u8 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply H20 with λ x5 x6 . x6 ⊆ u8.
The subproof is completed by applying unknownprop_c3570fdaac6dce8476fd6088341043cdfd2e266e0f12a2952f0077d35d442a0e.
Apply L12.
Apply Subq_tra with x1, x2, u8 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply H20 with λ x5 x6 . x6 ⊆ u8.
The subproof is completed by applying unknownprop_49b9e33c7aa67e5bb6441981bef50aeb406093cecddd64bc06e3dd9f061c9759.
Apply L12.
Apply H20 with λ x5 x6 . x1 ⊆ x5.
The subproof is completed by applying H10.
■ |
|