Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > prop | GIF version |
Description: A positive real is an ordered pair of a lower cut and an upper cut. (Contributed by Jim Kingdon, 27-Sep-2019.) |
Ref | Expression |
---|---|
prop | ⊢ (𝐴 ∈ P → 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | npsspw 7422 | . . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q) | |
2 | 1 | sseli 3143 | . . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q)) |
3 | 1st2nd2 6152 | . . 3 ⊢ (𝐴 ∈ (𝒫 Q × 𝒫 Q) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | |
4 | 2, 3 | syl 14 | . 2 ⊢ (𝐴 ∈ P → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
5 | eleq1 2233 | . . 3 ⊢ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 → (𝐴 ∈ P ↔ 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P)) | |
6 | 5 | biimpcd 158 | . 2 ⊢ (𝐴 ∈ P → (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 → 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P)) |
7 | 4, 6 | mpd 13 | 1 ⊢ (𝐴 ∈ P → 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P) |
Copyright terms: Public domain | W3C validator |