P. 382 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38101-38200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mon1psubm 38101	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑃)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈))
Theorem	deg1mhm 38102	Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝑌 = ((mulGrp‘𝑃) ↾s (𝐵 ∖ { 0 }))    &   ⊢ 𝑁 = (ℂfld ↾s ℕ0)    ⇒   ⊢ (𝑅 ∈ Domn → (𝐷 ↾ (𝐵 ∖ { 0 })) ∈ (𝑌 MndHom 𝑁))
Theorem	cytpfn 38103	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ CytP Fn ℕ
Theorem	cytpval 38104*	Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ 𝑂 = (od‘𝑇)    &   ⊢ 𝑃 = (Poly1‘ℂfld)    &   ⊢ 𝑋 = (var1‘ℂfld)    &   ⊢ 𝑄 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ (𝑁 ∈ ℕ → (CytP‘𝑁) = (𝑄 Σg (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟)))))
20.25.50  Miscellaneous topology
Theorem	fgraphopab 38105*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)})
Theorem	fgraphxp 38106*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)})
Theorem	hausgraph 38107	The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾)))
Syntax	ctopsep 38108	The class of separable toplogies.
class TopSep
Syntax	ctoplnd 38109	The class of Lindelöf toplogies.
class TopLnd
Definition	df-topsep 38110*	A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
⊢ TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)}
Definition	df-toplnd 38111*	A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))}
20.26  Mathbox for Jon Pennant
Theorem	ioounsn 38112	The closure of the upper end of an open real interval. (Contributed by Jon Pennant, 8-Jun-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵))
Theorem	iocunico 38113	Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶))
Theorem	iocinico 38114	The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵})
Theorem	iocmbl 38115	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol)
Theorem	cnioobibld 38116*	A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider 𝐹 = (𝑥 ∈ (0(,)1) ↦ (1 / 𝑥)). See cniccibl 23652 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	itgpowd 38117*	The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1)))
Theorem	arearect 38118	The area of a rectangle whose sides are parallel to the coordinate axes in (ℝ × ℝ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝐶 ≤ 𝐷    &   ⊢ 𝑆 = ((𝐴[,]𝐵) × (𝐶[,]𝐷))    ⇒   ⊢ (area‘𝑆) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))
Theorem	areaquad 38119*	The area of a quadrilateral with two sides which are parallel to the y-axis in (ℝ × ℝ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    &   ⊢ 𝐸 ∈ ℝ    &   ⊢ 𝐹 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐶 ≤ 𝐸    &   ⊢ 𝐷 ≤ 𝐹    &   ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))    &   ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}    ⇒   ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
20.27  Mathbox for Richard Penner
20.27.1  Short Studies
20.27.1.1  Additional work on conditional logical operator
Theorem	ifpan123g 38120	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
Theorem	ifpan23 38121	Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏)))
Theorem	ifpdfor2 38122	Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓))
Theorem	ifporcor 38123	Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.)
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑))
Theorem	ifpdfan2 38124	Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑))
Theorem	ifpancor 38125	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓))
Theorem	ifpdfor 38126	Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓))
Theorem	ifpdfan 38127	Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥))
Theorem	ifpbi2 38128	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃)))
Theorem	ifpbi3 38129	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓)))
Theorem	ifpim1 38130	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓))
Theorem	ifpnot 38131	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤))
Theorem	ifpid2 38132	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥))
Theorem	ifpim2 38133	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑))
Theorem	ifpbi23 38134	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃)))
Theorem	ifpdfbi 38135	Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓))
Theorem	ifpbiidcor 38136	Restatement of biid 251. (Contributed by RP, 25-Apr-2020.)
⊢ if-(𝜑, 𝜑, ¬ 𝜑)
Theorem	ifpbicor 38137	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	ifpxorcor 38138	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑))
Theorem	ifpbi1 38139	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)))
Theorem	ifpnot23 38140	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒))
Theorem	ifpnotnotb 38141	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpnorcor 38142	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑))
Theorem	ifpnancor 38143	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓))
Theorem	ifpnot23b 38144	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒))
Theorem	ifpbiidcor2 38145	Restatement of biid 251. (Contributed by RP, 25-Apr-2020.)
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑)
Theorem	ifpnot23c 38146	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒))
Theorem	ifpnot23d 38147	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpdfnan 38148	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤))
Theorem	ifpdfxor 38149	Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓))
Theorem	ifpbi12 38150	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏)))
Theorem	ifpbi13 38151	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃)))
Theorem	ifpbi123 38152	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂)))
Theorem	ifpidg 38153	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒)))))
Theorem	ifpid3g 38154	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓)))
Theorem	ifpid2g 38155	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpid1g 38156	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓)))
Theorem	ifpim23g 38157	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpim3 38158	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑))
Theorem	ifpnim1 38159	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑))
Theorem	ifpim4 38160	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑))
Theorem	ifpnim2 38161	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑))
Theorem	ifpim123g 38162	Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
Theorem	ifpim1g 38163	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃))))
Theorem	ifp1bi 38164	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))))
Theorem	ifpbi1b 38165	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒))
Theorem	ifpimimb 38166	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpororb 38167	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpananb 38168	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpnannanb 38169	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpor123g 38170	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂)))))
Theorem	ifpimim 38171	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpbibib 38172	Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpxorxorb 38173	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏)))
20.27.1.2  Sophisms
Theorem	rp-fakeimass 38174	A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
Theorem	rp-fakeanorass 38175	A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒))))
Theorem	rp-fakeoranass 38176	A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
Theorem	rp-fakenanass 38177	A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
Theorem	rp-fakeinunass 38178	A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
⊢ (𝐶 ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∪ 𝐶) = (𝐴 ∩ (𝐵 ∪ 𝐶)))
Theorem	rp-fakeuninass 38179	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
⊢ (𝐴 ⊆ 𝐶 ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐴 ∪ (𝐵 ∩ 𝐶)))
20.27.1.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 38180*	A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some 𝑛 ∈ ℕ0. (Contributed by Richard Penner, 3-Mar-2020.)
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0 (1...𝑛) ≈ 𝐴)
Theorem	rp-isfinite6 38181*	A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some 𝑛 ∈ ℕ. (Contributed by Richard Penner, 10-Mar-2020.)
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴))
20.27.1.4  Infinite Sets
Theorem	pwelg 38182*	The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵))
Theorem	pwinfig 38183*	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝐵 is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝐵 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝐵 ∖ Fin)))
Theorem	pwinfi2 38184	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑈 is a weak universe. (Contributed by RP, 21-Mar-2020.)
⊢ (𝑈 ∈ WUni → (𝐴 ∈ (𝑈 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑈 ∖ Fin)))
Theorem	pwinfi3 38185	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑇 is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → (𝐴 ∈ (𝑇 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑇 ∖ Fin)))
Theorem	pwinfi 38186	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin))
20.27.1.5  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 8278 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 5792, ordelinel 5863), chains of sets ordered by the proper subset relation (sorpssin 6987), various sets in the field of topology (inopn 20752, incld 20895, innei 20977, ... ) and "universal" classes like weak universes (wunin 9573, tskin 9619) and the class of all sets (inex1g 4834).
Theorem	fipjust 38187*	A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by Richard Penner, 1-Jan-2020.)
⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 ∩ 𝑣) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)
Theorem	cllem0 38188*	The class of all sets with property 𝜑(𝑧) is closed under the binary operation on sets defined in 𝑅(𝑥, 𝑦). (Contributed by Richard Penner, 3-Jan-2020.)
⊢ 𝑉 = {𝑧 ∣ 𝜑}    &   ⊢ 𝑅 ∈ 𝑈    &   ⊢ (𝑧 = 𝑅 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑧 = 𝑥 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜓)    ⇒   ⊢ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑅 ∈ 𝑉
Theorem	superficl 38189*	The class of all supersets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	superuncl 38190*	The class of all supersets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssficl 38191*	The class of all subsets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	ssuncl 38192*	The class of all subsets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssdifcl 38193*	The class of all subsets of a class is closed under class difference. (Contributed by Richard Penner, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴
Theorem	sssymdifcl 38194*	The class of all subsets of a class is closed under symmetric difference. (Contributed by Richard Penner, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴
Theorem	fiinfi 38195*	If two classes have the finite intersection property, then so does their intersection. (Contributed by Richard Penner, 1-Jan-2020.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶)
20.27.1.6  RP ADDTO: Subclasses and subsets
Theorem	rababg 38196	Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.)
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑})
20.27.1.7  RP ADDTO: The intersection of a class
Theorem	elintabg 38197*	Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elinintab 38198*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elmapintrab 38199*	Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐶 ⊆ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶))))
20.27.1.8  RP ADDTO: Theorems requiring subset and intersection existence
Theorem	elinintrab 38200*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = (𝐵 ∩ 𝑥) ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))))