Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-pss | Structured version Visualization version GIF version |
Description: Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 28135). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4076). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3951). Other possible definitions are given by dfpss2 4061 and dfpss3 4062. (Contributed by NM, 7-Feb-1996.) |
Ref | Expression |
---|---|
df-pss | ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wpss 3936 | . 2 wff 𝐴 ⊊ 𝐵 |
4 | 1, 2 | wss 3935 | . . 3 wff 𝐴 ⊆ 𝐵 |
5 | 1, 2 | wne 3016 | . . 3 wff 𝐴 ≠ 𝐵 |
6 | 4, 5 | wa 396 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
7 | 3, 6 | wb 207 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfpss2 4061 psseq1 4063 psseq2 4064 pssss 4071 pssne 4072 nssinpss 4232 pssdif 4325 0pss 4394 difsnpss 4734 ordelpss 6213 fisseneq 8718 ominf 8719 f1finf1o 8734 fofinf1o 8788 inf3lem2 9081 inf3lem4 9083 infeq5 9089 fin23lem31 9754 isf32lem6 9769 ipolt 17759 lssnle 18731 pgpfaclem2 19135 lspsncv0 19849 islbs3 19858 lbsextlem4 19864 lidlnz 19931 filssufilg 22449 alexsubALTlem4 22588 ppiltx 25682 ex-pss 28135 ch0pss 29150 nepss 32846 dfon2 32935 relowlpssretop 34528 finxpreclem3 34557 fin2solem 34760 lshpnelb 36002 lshpcmp 36006 lsatssn0 36020 lcvbr3 36041 lsatcv0 36049 lsat0cv 36051 lcvexchlem1 36052 islshpcv 36071 lkrpssN 36181 lkreqN 36188 osumcllem11N 36984 pexmidlem8N 36995 dochsordN 38392 dochsat 38401 dochshpncl 38402 dochexmidlem8 38485 mapdsord 38673 psspwb 38994 xppss12 38995 trelpss 40667 isomenndlem 42693 lvecpsslmod 44460 |
Copyright terms: Public domain | W3C validator |