![]() |
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 relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 27415). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 3740). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3621). Other possible definitions are given by dfpss2 3725 and dfpss3 3726. (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 3608 | . 2 wff 𝐴 ⊊ 𝐵 |
4 | 1, 2 | wss 3607 | . . 3 wff 𝐴 ⊆ 𝐵 |
5 | 1, 2 | wne 2823 | . . 3 wff 𝐴 ≠ 𝐵 |
6 | 4, 5 | wa 383 | . 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) |
7 | 3, 6 | wb 196 | 1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfpss2 3725 psseq1 3727 psseq2 3728 pssss 3735 pssne 3736 nssinpss 3889 pssdif 3978 0pss 4046 difsnpss 4370 ordelpss 5789 fisseneq 8212 ominf 8213 f1finf1o 8228 fofinf1o 8282 inf3lem2 8564 inf3lem4 8566 infeq5 8572 fin23lem31 9203 isf32lem6 9218 ipolt 17206 lssnle 18133 pgpfaclem2 18527 lspsncv0 19194 islbs3 19203 lbsextlem4 19209 lidlnz 19276 filssufilg 21762 alexsubALTlem4 21901 ppiltx 24948 ex-pss 27415 ch0pss 28432 nepss 31725 dfon2 31821 relowlpssretop 33342 finxpreclem3 33360 fin2solem 33525 lshpnelb 34589 lshpcmp 34593 lsatssn0 34607 lcvbr3 34628 lsatcv0 34636 lsat0cv 34638 lcvexchlem1 34639 islshpcv 34658 lkrpssN 34768 lkreqN 34775 osumcllem11N 35570 pexmidlem8N 35581 dochsordN 36980 dochsat 36989 dochshpncl 36990 dochexmidlem8 37073 mapdsord 37261 trelpss 38976 isomenndlem 41065 lvecpsslmod 42621 |
Copyright terms: Public domain | W3C validator |