![]() |
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 28213). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4028). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3898). Other possible definitions are given by dfpss2 4013 and dfpss3 4014. (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 3882 | . 2 wff 𝐴 ⊊ 𝐵 |
4 | 1, 2 | wss 3881 | . . 3 wff 𝐴 ⊆ 𝐵 |
5 | 1, 2 | wne 2987 | . . 3 wff 𝐴 ≠ 𝐵 |
6 | 4, 5 | wa 399 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
7 | 3, 6 | wb 209 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfpss2 4013 psseq1 4015 psseq2 4016 pssss 4023 pssne 4024 nssinpss 4183 pssdif 4280 0pss 4352 difsnpss 4700 ordelpss 6187 fisseneq 8713 ominf 8714 f1finf1o 8729 fofinf1o 8783 inf3lem2 9076 inf3lem4 9078 infeq5 9084 fin23lem31 9754 isf32lem6 9769 ipolt 17761 lssnle 18792 pgpfaclem2 19197 lspsncv0 19911 islbs3 19920 lbsextlem4 19926 lidlnz 19994 filssufilg 22516 alexsubALTlem4 22655 ppiltx 25762 ex-pss 28213 ch0pss 29228 nepss 33061 dfon2 33150 relowlpssretop 34781 finxpreclem3 34810 fin2solem 35043 lshpnelb 36280 lshpcmp 36284 lsatssn0 36298 lcvbr3 36319 lsatcv0 36327 lsat0cv 36329 lcvexchlem1 36330 islshpcv 36349 lkrpssN 36459 lkreqN 36466 osumcllem11N 37262 pexmidlem8N 37273 dochsordN 38670 dochsat 38679 dochshpncl 38680 dochexmidlem8 38763 mapdsord 38951 psspwb 39408 xppss12 39409 trelpss 41159 isomenndlem 43169 lvecpsslmod 44916 |
Copyright terms: Public domain | W3C validator |