![]() |
Metamath
Proof Explorer Theorem List (p. 403 of 443) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28486) |
![]() (28487-30011) |
![]() (30012-44298) |
Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||
Theorem | pm14.122b 40201* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | pm14.122c 40202* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | pm14.123a 40203* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | pm14.123b 40204* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | pm14.123c 40205* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | pm14.18 40206 | Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | iotaequ 40207* | Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (℩𝑥𝑥 = 𝑦) = 𝑦 | ||||||||||||||||||||||||||||||||
Theorem | iotavalb 40208* | Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6160. (Contributed by Andrew Salmon, 11-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦)) | ||||||||||||||||||||||||||||||||
Theorem | iotasbc5 40209* | Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | pm14.24 40210* | Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | iotavalsb 40211* | Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | sbiota1 40212 | Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | sbaniota 40213 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | eubiOLD 40214 | Obsolete proof of eubi 2603 as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | iotasbcq 40215 | Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒)) | ||||||||||||||||||||||||||||||||
Theorem | elnev 40216* | Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ V ↔ {𝑥 ∣ ¬ 𝑥 = 𝐴} ≠ V) | ||||||||||||||||||||||||||||||||
Theorem | rusbcALT 40217 | A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V | ||||||||||||||||||||||||||||||||
Theorem | compel 40218 | Equivalence between two ways of saying "is a member of the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) | ||||||||||||||||||||||||||||||||
Theorem | compeq 40219* | Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴} | ||||||||||||||||||||||||||||||||
Theorem | compne 40220 | The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.) | ||||||||||||||||||||||||||||||
⊢ (V ∖ 𝐴) ≠ 𝐴 | ||||||||||||||||||||||||||||||||
Theorem | compneOLD 40221 | Obsolete proof of compne 40220 as of 11-Nov-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (V ∖ 𝐴) ≠ 𝐴 | ||||||||||||||||||||||||||||||||
Theorem | compab 40222 | Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) | ||||||||||||||||||||||||||||||
⊢ (V ∖ {𝑧 ∣ 𝜑}) = {𝑧 ∣ ¬ 𝜑} | ||||||||||||||||||||||||||||||||
Theorem | conss2 40223 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴)) | ||||||||||||||||||||||||||||||||
Theorem | conss1 40224 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴) | ||||||||||||||||||||||||||||||||
Theorem | ralbidar 40225 | More general form of ralbida 3171. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||||||||||||||||||||||||||||||||
Theorem | rexbidar 40226 | More general form of rexbida 3255. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||||||||||||||||||||||||||||||||
Theorem | dropab1 40227 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥 𝑥 = 𝑦 → {〈𝑥, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ 𝜑}) | ||||||||||||||||||||||||||||||||
Theorem | dropab2 40228 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥 𝑥 = 𝑦 → {〈𝑧, 𝑥〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜑}) | ||||||||||||||||||||||||||||||||
Theorem | ipo0 40229 | If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ ( I Po 𝐴 ↔ 𝐴 = ∅) | ||||||||||||||||||||||||||||||||
Theorem | ifr0 40230 | A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅) | ||||||||||||||||||||||||||||||||
Theorem | ordpss 40231 | ordelpss 6054 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.) | ||||||||||||||||||||||||||||||
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵)) | ||||||||||||||||||||||||||||||||
Theorem | fvsb 40232* | Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) | ||||||||||||||||||||||||||||||
⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | fveqsb 40233* | Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) | ||||||||||||||||||||||||||||||
⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | xpexb 40234 | A Cartesian product exists iff its converse does. Corollary 6.9(1) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 × 𝐵) ∈ V ↔ (𝐵 × 𝐴) ∈ V) | ||||||||||||||||||||||||||||||||
Theorem | trelpss 40235 | An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5387, ax-reg 8849 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.) | ||||||||||||||||||||||||||||||
⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴) | ||||||||||||||||||||||||||||||||
Theorem | addcomgi 40236 | Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012.) (Revised by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||||||||||||||||||||||||||||||||
Syntax | cplusr 40237 | Introduce the operation of vector addition. | ||||||||||||||||||||||||||||||
class +𝑟 | ||||||||||||||||||||||||||||||||
Syntax | cminusr 40238 | Introduce the operation of vector subtraction. | ||||||||||||||||||||||||||||||
class -𝑟 | ||||||||||||||||||||||||||||||||
Syntax | ctimesr 40239 | Introduce the operation of scalar multiplication. | ||||||||||||||||||||||||||||||
class .𝑣 | ||||||||||||||||||||||||||||||||
Syntax | cptdfc 40240 | PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems. | ||||||||||||||||||||||||||||||
class PtDf(𝐴, 𝐵) | ||||||||||||||||||||||||||||||||
Syntax | crr3c 40241 | RR3 is a class. | ||||||||||||||||||||||||||||||
class RR3 | ||||||||||||||||||||||||||||||||
Syntax | cline3 40242 | line3 is a class. | ||||||||||||||||||||||||||||||
class line3 | ||||||||||||||||||||||||||||||||
Definition | df-addr 40243* | Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ +𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣)))) | ||||||||||||||||||||||||||||||||
Definition | df-subr 40244* | Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ -𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣)))) | ||||||||||||||||||||||||||||||||
Definition | df-mulv 40245* | Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ .𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣)))) | ||||||||||||||||||||||||||||||||
Theorem | addrval 40246* | Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣)))) | ||||||||||||||||||||||||||||||||
Theorem | subrval 40247* | Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣)))) | ||||||||||||||||||||||||||||||||
Theorem | mulvval 40248* | Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣)))) | ||||||||||||||||||||||||||||||||
Theorem | addrfv 40249 | Vector addition at a value. The operation takes each vector 𝐴 and 𝐵 and forms a new vector whose values are the sum of each of the values of 𝐴 and 𝐵. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴+𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) + (𝐵‘𝐶))) | ||||||||||||||||||||||||||||||||
Theorem | subrfv 40250 | Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶))) | ||||||||||||||||||||||||||||||||
Theorem | mulvfv 40251 | Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴.𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶))) | ||||||||||||||||||||||||||||||||
Theorem | addrfn 40252 | Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) Fn ℝ) | ||||||||||||||||||||||||||||||||
Theorem | subrfn 40253 | Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) Fn ℝ) | ||||||||||||||||||||||||||||||||
Theorem | mulvfn 40254 | Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) Fn ℝ) | ||||||||||||||||||||||||||||||||
Theorem | addrcom 40255 | Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝐵+𝑟𝐴)) | ||||||||||||||||||||||||||||||||
Definition | df-ptdf 40256* | Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
⊢ PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3})) | ||||||||||||||||||||||||||||||||
Definition | df-rr3 40257 | Define the set of all points RR3. We define each point 𝐴 as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
⊢ RR3 = (ℝ ↑𝑚 {1, 2, 3}) | ||||||||||||||||||||||||||||||||
Definition | df-line3 40258* | Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
⊢ line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))} | ||||||||||||||||||||||||||||||||
We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019). Alan's first contribution to Metamath was a shorter proof for tfrlem8 7822 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: https://us.metamath.org/other.html#completeusersproof. His virtual deduction method is explained in the comment for wvd1 40351. Below are some excerpts from his first emails to NM in 2007: ...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the Metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me.... ...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics, construct axioms based on experimental results, and to cast all of physics into a collection of axioms and theorems. Maybe this has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way.... ...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof.... | ||||||||||||||||||||||||||||||||
Theorem | idiALT 40259 | Placeholder for idi 1. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||||||||||||||||||||||||||||||||
Theorem | exbir 40260 | Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 40635. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||||||||||||||||||||||||||||||||
Theorem | 3impexpbicom 40261 | Version of 3impexp 1338 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) | ||||||||||||||||||||||||||||||||
Theorem | 3impexpbicomi 40262 | Inference associated with 3impexpbicom 40261. Derived automatically from 3impexpbicomiVD 40640. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | bi1imp 40263 | Importation inference similar to imp 398, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||||||||||||||||||||||||||||||||
Theorem | bi2imp 40264 | Importation inference similar to imp 398, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||||||||||||||||||||||||||||||||
Theorem | bi3impb 40265 | Similar to 3impb 1095 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi3impa 40266 | Similar to 3impa 1090 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi23impib 40267 | 3impib 1096 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13impib 40268 | 3impib 1096 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi123impib 40269 | 3impib 1096 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13impia 40270 | 3impia 1097 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi123impia 40271 | 3impia 1097 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi33imp12 40272 | 3imp 1091 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi23imp13 40273 | 3imp 1091 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ↔ (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13imp23 40274 | 3imp 1091 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13imp2 40275 | Similar to 3imp 1091 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi12imp3 40276 | Similar to 3imp 1091 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi23imp1 40277 | Similar to 3imp 1091 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ↔ (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi123imp0 40278 | Similar to 3imp 1091 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | 4animp1 40279 | A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||||||||||||||||||||||||||||||||
Theorem | 4an31 40280 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
⊢ ((((𝜒 ∧ 𝜓) ∧ 𝜑) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||||||||||||||||||||||||||||||||
Theorem | 4an4132 40281 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
⊢ ((((𝜃 ∧ 𝜒) ∧ 𝜓) ∧ 𝜑) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||||||||||||||||||||||||||||||||
Theorem | expcomdg 40282 | Biconditional form of expcomd 409. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜒 → (𝜓 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | iidn3 40283 | idn3 40397 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜒))) | ||||||||||||||||||||||||||||||||
Theorem | ee222 40284 | e222 40418 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||||||||||||||||||||||||||||||||
Theorem | ee3bir 40285 | Right-biconditional form of e3 40519 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜏 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||||||||||||||||||||||||||||||||
Theorem | ee13 40286 | e13 40530 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||||||||||||||||||||||||||||||||
Theorem | ee121 40287 | e121 40438 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||||||||||||||||||||||||||||||||
Theorem | ee122 40288 | e122 40435 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜏)) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||||||||||||||||||||||||||||||||
Theorem | ee333 40289 | e333 40515 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁))) | ||||||||||||||||||||||||||||||||
Theorem | ee323 40290 | e323 40548 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁))) | ||||||||||||||||||||||||||||||||
Theorem | 3ornot23 40291 | If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 40629. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)) | ||||||||||||||||||||||||||||||||
Theorem | orbi1r 40292 | orbi1 901 with order of disjuncts reversed. Derived from orbi1rVD 40630. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | 3orbi123 40293 | pm4.39 959 with a 3-conjunct antecedent. This proof is 3orbi123VD 40632 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) | ||||||||||||||||||||||||||||||||
Theorem | syl5imp 40294 | Closed form of syl5 34. Derived automatically from syl5impVD 40645. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒)))) | ||||||||||||||||||||||||||||||||
Theorem | impexpd 40295 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. After the
User's Proof was completed, it was minimized. The completed User's Proof
before minimization is not shown. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | com3rgbi 40296 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) ↔ (𝜒 → (𝜑 → (𝜓 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | impexpdcom 40297 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | ee1111 40298 |
Non-virtual deduction form of e1111 40457. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ (𝜑 → 𝜂) | ||||||||||||||||||||||||||||||||
Theorem | pm2.43bgbi 40299 |
Logical equivalence of a 2-left-nested implication and a 1-left-nested
implicated
when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) ↔ (𝜓 → (𝜑 → 𝜒))) | ||||||||||||||||||||||||||||||||
Theorem | pm2.43cbi 40300 |
Logical equivalence of a 3-left-nested implication and a 2-left-nested
implicated when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is
a Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof
(not shown) was minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃)))) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |