![]() |
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 29610). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4097). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3962). Other possible definitions are given by dfpss2 4082 and dfpss3 4083. (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 3946 | . 2 wff 𝐴 ⊊ 𝐵 |
4 | 1, 2 | wss 3945 | . . 3 wff 𝐴 ⊆ 𝐵 |
5 | 1, 2 | wne 2940 | . . 3 wff 𝐴 ≠ 𝐵 |
6 | 4, 5 | wa 396 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
7 | 3, 6 | wb 205 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfpss2 4082 psseq1 4084 psseq2 4085 pssss 4092 pssne 4093 nssinpss 4253 pssdif 4363 0pss 4441 difsnpss 4804 ordelpss 6382 fisseneq 9242 ominf 9243 ominfOLD 9244 f1finf1o 9256 f1finf1oOLD 9257 fofinf1o 9312 inf3lem2 9608 inf3lem4 9610 infeq5 9616 fin23lem31 10322 isf32lem6 10337 ipolt 18472 lssnle 19508 pgpfaclem2 19913 lspsncv0 20710 islbs3 20719 lbsextlem4 20725 lidlnz 20801 filssufilg 23346 alexsubALTlem4 23485 ppiltx 26610 ex-pss 29610 ch0pss 30625 nepss 34581 dfon2 34658 relowlpssretop 36113 finxpreclem3 36142 fin2solem 36342 lshpnelb 37723 lshpcmp 37727 lsatssn0 37741 lcvbr3 37762 lsatcv0 37770 lsat0cv 37772 lcvexchlem1 37773 islshpcv 37792 lkrpssN 37902 lkreqN 37909 osumcllem11N 38706 pexmidlem8N 38717 dochsordN 40114 dochsat 40123 dochshpncl 40124 dochexmidlem8 40207 mapdsord 40395 psspwb 40925 xppss12 40926 omssrncard 42126 trelpss 43049 isomenndlem 45083 lvecpsslmod 46900 |
Copyright terms: Public domain | W3C validator |