Let X be given.
We will prove {X} ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ {X}, x ∈ b) ∧ (∀b1 ∈ {X}, ∀b2 ∈ {X}, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ {X}, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply andI to the current goal.
Apply andI to the current goal.
Let b be given.
Assume Hb: b ∈ {X}.
We will prove b ∈ 𝒫 X.
We prove the intermediate claim HbX: b = X.
An exact proof term for the current goal is (SingE X b Hb).
rewrite the current goal using HbX (from left to right).
An exact proof term for the current goal is (Self_In_Power X).
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃b ∈ {X}, x ∈ b.
We use X to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (SingI X).
An exact proof term for the current goal is HxX.
Let b1 be given.
Assume Hb1: b1 ∈ {X}.
Let b2 be given.
Assume Hb2: b2 ∈ {X}.
Let x be given.
Assume Hxb1: x ∈ b1.
Assume Hxb2: x ∈ b2.
We will prove ∃b3 ∈ {X}, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim Hb1X: b1 = X.
An exact proof term for the current goal is (SingE X b1 Hb1).
We prove the intermediate claim Hb2X: b2 = X.
An exact proof term for the current goal is (SingE X b2 Hb2).
We use X to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (SingI X).
We will prove x ∈ X ∧ X ⊆ b1 ∩ b2.
Apply andI to the current goal.
rewrite the current goal using Hb1X (from right to left).
An exact proof term for the current goal is Hxb1.
Let y be given.
Assume HyX: y ∈ X.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1X (from left to right).
An exact proof term for the current goal is HyX.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2X (from left to right).
An exact proof term for the current goal is HyX.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
∎