P. 444 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44301-44400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	finona1cl 44301	The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.)
⊢ (𝑁 ∈ (On ∩ Fin) → (𝑁 +o 1o) ∈ (On ∩ Fin))
Theorem	finonex 44302	The finite ordinals are a set. See also onprc 7781 and fiprc 9055 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.)
⊢ (On ∩ Fin) ∈ V
Theorem	fzunt 44303	Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzuntd 44304	Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzunt1d 44305	Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzuntgd 44306	Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐿 + 1))    &   ⊢ (𝜑 → 𝐿 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
21.38.4.1  Additional work on conditional logical operator
Theorem	ifpan123g 44307	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
Theorem	ifpan23 44308	Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏)))
Theorem	ifpdfor2 44309	Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓))
Theorem	ifporcor 44310	Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.)
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑))
Theorem	ifpdfan2 44311	Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑))
Theorem	ifpancor 44312	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓))
Theorem	ifpdfor 44313	Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓))
Theorem	ifpdfan 44314	Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥))
Theorem	ifpbi2 44315	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃)))
Theorem	ifpbi3 44316	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓)))
Theorem	ifpim1 44317	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓))
Theorem	ifpnot 44318	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤))
Theorem	ifpid2 44319	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥))
Theorem	ifpim2 44320	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑))
Theorem	ifpbi23 44321	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃)))
Theorem	ifpbiidcor 44322	Restatement of biid 264. (Contributed by RP, 25-Apr-2020.)
⊢ if-(𝜑, 𝜑, ¬ 𝜑)
Theorem	ifpbicor 44323	Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	ifpxorcor 44324	Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑))
Theorem	ifpbi1 44325	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)))
Theorem	ifpnot23 44326	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒))
Theorem	ifpnotnotb 44327	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpnorcor 44328	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑))
Theorem	ifpnancor 44329	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓))
Theorem	ifpnot23b 44330	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒))
Theorem	ifpbiidcor2 44331	Restatement of biid 264. (Contributed by RP, 25-Apr-2020.)
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑)
Theorem	ifpnot23c 44332	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒))
Theorem	ifpnot23d 44333	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpdfnan 44334	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤))
Theorem	ifpdfxor 44335	Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓))
Theorem	ifpbi12 44336	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏)))
Theorem	ifpbi13 44337	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃)))
Theorem	ifpbi123 44338	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂)))
Theorem	ifpidg 44339	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒)))))
Theorem	ifpid3g 44340	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓)))
Theorem	ifpid2g 44341	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpid1g 44342	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓)))
Theorem	ifpim23g 44343	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpim3 44344	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑))
Theorem	ifpnim1 44345	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑))
Theorem	ifpim4 44346	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑))
Theorem	ifpnim2 44347	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑))
Theorem	ifpim123g 44348	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 44349	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃))))
Theorem	ifp1bi 44350	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))))
Theorem	ifpbi1b 44351	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒))
Theorem	ifpimimb 44352	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpororb 44353	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpananb 44354	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpnannanb 44355	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpor123g 44356	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂)))))
Theorem	ifpimim 44357	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpbibib 44358	Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpxorxorb 44359	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏)))
21.38.4.2  Sophisms
Theorem	rp-fakeimass 44360	A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))))
Theorem	rp-fakeanorass 44361	A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.)
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒))))
Theorem	rp-fakeoranass 44362	A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
Theorem	rp-fakeinunass 44363	A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.)
⊢ (𝐶 ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∪ 𝐶) = (𝐴 ∩ (𝐵 ∪ 𝐶)))
Theorem	rp-fakeuninass 44364	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.)
⊢ (𝐴 ⊆ 𝐶 ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐴 ∪ (𝐵 ∩ 𝐶)))
21.38.4.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 44365*	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 RP, 3-Mar-2020.)
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ℕ0 (1...𝑛) ≈ 𝐴)
Theorem	rp-isfinite6 44366*	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 RP, 10-Mar-2020.)
⊢ (𝐴 ∈ Fin ↔ (𝐴 = ∅ ∨ ∃𝑛 ∈ ℕ (1...𝑛) ≈ 𝐴))
21.38.4.4  General Observations
Theorem	intabssd 44367*	When for each element 𝑦 there is a subset 𝐴 which may substituted for 𝑥 such that 𝑦 satisfying 𝜒 implies 𝑥 satisfies 𝜓 then the intersection of all 𝑥 that satisfy 𝜓 is a subclass the intersection of all 𝑦 that satisfy 𝜒. (Contributed by RP, 17-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑦)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ 𝜓} ⊆ ∩ {𝑦 ∣ 𝜒})
Theorem	eu0 44368*	There is only one empty set. (Contributed by RP, 1-Oct-2023.)
⊢ (∀𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	epelon2 44369	Over the ordinal numbers, one may define the relation 𝐴 E 𝐵 iff 𝐴 ∈ 𝐵 and one finds that, under this ordering, On is a well-ordered class, see epweon 7778. This is a weak form of epelg 5560 which only requires that we know 𝐵 to be a set. (Contributed by RP, 27-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	ontric3g 44370*	For all 𝑥, 𝑦 ∈ On, one and only one of the following hold: 𝑥 ∈ 𝑦, 𝑦 = 𝑥, or 𝑦 ∈ 𝑥. This is a transparent strict trichotomy. (Contributed by RP, 27-Sep-2023.)
⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On ((𝑥 ∈ 𝑦 ↔ ¬ (𝑦 = 𝑥 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 = 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)) ∧ (𝑦 ∈ 𝑥 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 = 𝑥)))
Theorem	dfsucon 44371*	𝐴 is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023.)
⊢ ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	snen1g 44372	A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ V)
Theorem	snen1el 44373	A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ {𝐴})
Theorem	sn1dom 44374	A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴} ≼ 1o
Theorem	pr2dom 44375	An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴, 𝐵} ≼ 2o
Theorem	tr3dom 44376	An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.)
⊢ {𝐴, 𝐵, 𝐶} ≼ 3o
Theorem	ensucne0 44377	A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.)
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅)
Theorem	ensucne0OLD 44378	A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅)
Theorem	dfom6 44379	Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.)
⊢ ω = ∪ (On ∩ Fin)
Theorem	infordmin 44380	ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.)
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥
Theorem	iscard4 44381	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card)
Theorem	minregex 44382*	Given any cardinal number 𝐴, there exists an argument 𝑥, which yields the least regular uncountable value of ℵ which is greater to or equal to 𝐴. This proof uses AC. (Contributed by RP, 23-Nov-2023.)
⊢ (𝐴 ∈ (ran card ∖ ω) → ∃𝑥 ∈ On 𝑥 = ∩ {𝑦 ∈ On ∣ (∅ ∈ 𝑦 ∧ 𝐴 ⊆ (ℵ‘𝑦) ∧ (cf‘(ℵ‘𝑦)) = (ℵ‘𝑦))})
Theorem	minregex2 44383*	Given any cardinal number 𝐴, there exists an argument 𝑥, which yields the least regular uncountable value of ℵ which dominates 𝐴. This proof uses AC. (Contributed by RP, 24-Nov-2023.)
⊢ (𝐴 ∈ (ran card ∖ ω) → ∃𝑥 ∈ On 𝑥 = ∩ {𝑦 ∈ On ∣ (∅ ∈ 𝑦 ∧ 𝐴 ≼ (ℵ‘𝑦) ∧ (cf‘(ℵ‘𝑦)) = (ℵ‘𝑦))})
Theorem	iscard5 44384*	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	elrncard 44385*	Let us define a cardinal number to be an element 𝐴 ∈ On such that 𝐴 is not equipotent with any 𝑥 ∈ 𝐴. (Contributed by RP, 1-Oct-2023.)
⊢ (𝐴 ∈ ran card ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	harval3 44386*	(har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	harval3on 44387*	For any ordinal number 𝐴 let (har‘𝐴) denote the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ On → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	omssrncard 44388	All natural numbers are cardinals. (Contributed by RP, 1-Oct-2023.)
⊢ ω ⊆ ran card
Theorem	0iscard 44389	0 is a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ ∅ ∈ ran card
Theorem	1iscard 44390	1 is a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ 1o ∈ ran card
Theorem	omiscard 44391	ω is a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ ω ∈ ran card
Theorem	sucomisnotcard 44392	ω +o 1o is not a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ ¬ (ω +o 1o) ∈ ran card
Theorem	nna1iscard 44393	For any natural number, the add one operation is results in a cardinal number. (Contributed by RP, 1-Oct-2023.)
⊢ (𝑁 ∈ ω → (𝑁 +o 1o) ∈ ran card)
Theorem	har2o 44394	The least cardinal greater than 2 is 3. (Contributed by RP, 5-Nov-2023.)
⊢ (har‘2o) = 3o
Theorem	en2pr 44395*	A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.)
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦))
Theorem	pr2cv 44396	If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	pr2el1 44397	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵})
Theorem	pr2cv1 44398	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V)
Theorem	pr2el2 44399	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵})
Theorem	pr2cv2 44400	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V)