HomeTheorem List (p. 364 of 509)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 364 of 509) | < 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: | Metamath Proof Explorer
(1-31407) |
Hilbert Space Explorer
(31408-32930) |
Users' Mathboxes
(32931-50831) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | untangtr 36301* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
| ⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦)) | ||
| Theorem | 3jaodd 36302 | Double deduction form of 3jaoi 1454. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂))) | ||
| Theorem | 3orit 36303 | Closed form of 3ori 1451. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)) | ||
| Theorem | biimpexp 36304 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
| ⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒))) | ||
| Theorem | nepss 36305 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
| ⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵)) | ||
| Theorem | 3ccased 36306 | Triple disjunction form of ccased 1054. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓)) ⇒ ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓)) | ||
| Theorem | dfso3 36307* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
| ⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
| Theorem | brtpid1 36308 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵 | ||
| Theorem | brtpid2 36309 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵 | ||
| Theorem | brtpid3 36310 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵 | ||
| Theorem | iota5f 36311* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
| Theorem | jath 36312 | Closed form of ja 188. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
| ⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) | ||
| Theorem | xpab 36313* | Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)} | ||
| Theorem | nnuni 36314 | The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.) |
| ⊢ (𝐴 ∈ ω → ∪ 𝐴 ∈ ω) | ||
| Theorem | sqdivzi 36315 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
| Theorem | supfz 36316 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
| Theorem | inffz 36317 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
| Theorem | fz0n 36318 | The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0)) | ||
| Theorem | shftvalg 36319 | Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
| Theorem | divcnvlin 36320* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
| Theorem | climlec3 36321* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | iexpire 36322 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
| ⊢ (i↑𝑐i) ∈ ℝ | ||
| Theorem | bcneg1 36323 | The binomial coefficient over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0) | ||
| Theorem | bcm1nt 36324 | The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾)))) | ||
| Theorem | bcprod 36325* | A product identity for binomial coefficients. (Contributed by Scott Fenton, 23-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) | ||
| Theorem | bccolsum 36326* | A column-sum rule for binomial coefficients. (Contributed by Scott Fenton, 24-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1))) | ||
| Theorem | iprodefisumlem 36327 | Lemma for iprodefisum 36328. (Contributed by Scott Fenton, 11-Feb-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹))) | ||
| Theorem | iprodefisum 36328* | Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (exp‘𝐵) = (exp‘Σ𝑘 ∈ 𝑍 𝐵)) | ||
| Theorem | iprodgam 36329* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
| ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) | ||
| Theorem | faclimlem1 36330* | Lemma for faclim 36333. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))) | ||
| Theorem | faclimlem2 36331* | Lemma for faclim 36333. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1)) | ||
| Theorem | faclimlem3 36332 | Lemma for faclim 36333. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵))))) | ||
| Theorem | faclim 36333* | An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))) ⇒ ⊢ (𝐴 ∈ ℕ0 → seq1( · , 𝐹) ⇝ (!‘𝐴)) | ||
| Theorem | iprodfac 36334* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘)))) | ||
| Theorem | faclim2 36335* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) ⇒ ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1) | ||
| Theorem | gcd32 36336 | Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐶) = ((𝐴 gcd 𝐶) gcd 𝐵)) | ||
| Theorem | gcdabsorb 36337 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵)) | ||
| Theorem | dftr6 36338 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E ))) | ||
| Theorem | coep 36339* | Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥) | ||
| Theorem | coepr 36340* | Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵) | ||
| Theorem | dffr5 36341 | A quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 11-Apr-2011.) (Proof shortened by Scott Fenton, 26-Aug-2026.) |
| ⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅))) | ||
| Theorem | dfso2 36342 | Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
| ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) | ||
| Theorem | br8 36343* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌)) | ||
| Theorem | br6 36344* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁)) | ||
| Theorem | br4 36345* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏)) | ||
| Theorem | cnvco1 36346 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴) | ||
| Theorem | cnvco2 36347 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴) | ||
| Theorem | eldm3 36348 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
| ⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) | ||
| Theorem | elrn3 36349 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
| ⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅) | ||
| Theorem | pocnv 36350 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
| Theorem | socnv 36351 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) | ||
| Theorem | elintfv 36352* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ 𝑋 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦))) | ||
| Theorem | funpsstri 36353 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
| ⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹)) | ||
| Theorem | fundmpss 36354 | If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺)) | ||
| Theorem | funsseq 36355 | Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺)) | ||
| Theorem | fununiq 36356 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
| Theorem | funbreq 36357 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶)) | ||
| Theorem | br1steq 36358 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴) | ||
| Theorem | br2ndeq 36359 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵) | ||
| Theorem | dfdm5 36360 | Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴) | ||
| Theorem | dfrn5 36361 | Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴) | ||
| Theorem | opelco3 36362 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
| ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) | ||
| Theorem | elima4 36363 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
| ⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅) | ||
| Theorem | fv1stcnv 36364 | The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
| ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩) | ||
| Theorem | fv2ndcnv 36365 | The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = ⟨𝑋, 𝑌⟩) | ||
| Theorem | elpotr 36366* | A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.) |
| ⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴) | ||
| Theorem | dford5reg 36367 | Given ax-reg 9568, an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011.) |
| ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E Or 𝐴)) | ||
| Theorem | dfon2lem1 36368 | Lemma for dfon2 36377. (Contributed by Scott Fenton, 28-Feb-2011.) |
| ⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)} | ||
| Theorem | dfon2lem2 36369* | Lemma for dfon2 36377. (Contributed by Scott Fenton, 28-Feb-2011.) |
| ⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴 | ||
| Theorem | dfon2lem3 36370* | Lemma for dfon2 36377. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧))) | ||
| Theorem | dfon2lem4 36371* | Lemma for dfon2 36377. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
| Theorem | dfon2lem5 36372* | Lemma for dfon2 36377. Two sets satisfying the new definition also satisfy trichotomy with respect to ∈. (Contributed by Scott Fenton, 25-Feb-2011.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) | ||
| Theorem | dfon2lem6 36373* | Lemma for dfon2 36377. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.) |
| ⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆)) | ||
| Theorem | dfon2lem7 36374* | Lemma for dfon2 36377. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵))) | ||
| Theorem | dfon2lem8 36375* | Lemma for dfon2 36377. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.) |
| ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)) | ||
| Theorem | dfon2lem9 36376* | Lemma for dfon2 36377. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.) |
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴) | ||
| Theorem | dfon2 36377* | On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.) |
| ⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} | ||
| Theorem | rdgprc0 36378 | The value of the recursive definition generator at ∅ when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (¬ 𝐼 ∈ V → (rec(𝐹, 𝐼)‘∅) = ∅) | ||
| Theorem | rdgprc 36379 | The value of the recursive definition generator when 𝐼 is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (¬ 𝐼 ∈ V → rec(𝐹, 𝐼) = rec(𝐹, ∅)) | ||
| Theorem | dfrdg2 36380* | Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}) | ||
| Theorem | dfrdg3 36381* | Generalization of dfrdg2 36380 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐼 ∈ V, 𝐼, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} | ||
| Theorem | axextdfeq 36382 | A version of ax-ext 2734 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
| ⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤))) | ||
| Theorem | ax8dfeq 36383 | A version of ax-8 2147 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
| ⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦)) | ||
| Theorem | axextdist 36384 | ax-ext 2734 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) | ||
| Theorem | axextbdist 36385 | axextb 2737 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) | ||
| Theorem | 19.12b 36386* | Version of 19.12vv 2378 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓)) | ||
| Theorem | exnel 36387 | There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦 | ||
| Theorem | distel 36388 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5417 and elirrv 9573.) (Contributed by Scott Fenton, 15-Dec-2010.) |
| ⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦) | ||
| Theorem | axextndbi 36389 | axextnd 10604 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
| ⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | ||
| Theorem | hbntg 36390 | A more general form of hbnt 2329. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑)) | ||
| Theorem | hbimtg 36391 | A more general and closed form of hbim 2334. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃))) | ||
| Theorem | hbaltg 36392 | A more general and closed form of hbal 2204. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓)) | ||
| Theorem | hbng 36393 | A more general form of hbn 2330. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (𝜑 → ∀𝑥𝜓) ⇒ ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑) | ||
| Theorem | hbimg 36394 | A more general form of hbim 2334. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜃) ⇒ ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃)) | ||
| Syntax | cwsuc 36395 | Declare the syntax for well-founded successor. |
| class wsuc(𝑅, 𝐴, 𝑋) | ||
| Syntax | cwlim 36396 | Declare the syntax for well-founded limit class. |
| class WLim(𝑅, 𝐴) | ||
| Definition | df-wsuc 36397 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅) | ||
| Definition | df-wlim 36398* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))} | ||
| Theorem | wsuceq123 36399 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌)) | ||
| Theorem | wsuceq1 36400 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |