naddcnfid2

Description: Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025)

		Ref	Expression
	Assertion	naddcnfid2	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to (X \times \{\emptyset\}) {+_{𝑜}}_{f} F = F$

Proof

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2		fconst6g	$⊢ \emptyset \in ω \to (X \times \{\emptyset\}) : X ⟶ ω$
3	1 2	mp1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to (X \times \{\emptyset\}) : X ⟶ ω$
4		simpl	$⊢ (X \in On \land S = dom (ω CNF X)) \to X \in On$
5	1	a1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to \emptyset \in ω$
6	4 5	fczfsuppd	$⊢ (X \in On \land S = dom (ω CNF X)) \to {finSupp}_{\emptyset} ((X \times \{\emptyset\}))$
7		simpr	$⊢ (X \in On \land S = dom (ω CNF X)) \to S = dom (ω CNF X)$
8	7	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (X \times \{\emptyset\} \in S \leftrightarrow X \times \{\emptyset\} \in dom (ω CNF X))$
9		eqid	$⊢ dom (ω CNF X) = dom (ω CNF X)$
10		omelon	$⊢ ω \in On$
11	10	a1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to ω \in On$
12	9 11 4	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (X \times \{\emptyset\} \in dom (ω CNF X) \leftrightarrow ((X \times \{\emptyset\}) : X ⟶ ω \land {finSupp}_{\emptyset} ((X \times \{\emptyset\}))))$
13	8 12	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (X \times \{\emptyset\} \in S \leftrightarrow ((X \times \{\emptyset\}) : X ⟶ ω \land {finSupp}_{\emptyset} ((X \times \{\emptyset\}))))$
14	3 6 13	mpbir2and	$⊢ (X \in On \land S = dom (ω CNF X)) \to X \times \{\emptyset\} \in S$
15		naddcnfcom	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (X \times \{\emptyset\} \in S \land F \in S)) \to (X \times \{\emptyset\}) {+_{𝑜}}_{f} F = F {+_{𝑜}}_{f} (X \times \{\emptyset\})$
16	15	ex	$⊢ (X \in On \land S = dom (ω CNF X)) \to ((X \times \{\emptyset\} \in S \land F \in S) \to (X \times \{\emptyset\}) {+_{𝑜}}_{f} F = F {+_{𝑜}}_{f} (X \times \{\emptyset\}))$
17	14 16	mpand	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \to (X \times \{\emptyset\}) {+_{𝑜}}_{f} F = F {+_{𝑜}}_{f} (X \times \{\emptyset\}))$
18	17	imp	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to (X \times \{\emptyset\}) {+_{𝑜}}_{f} F = F {+_{𝑜}}_{f} (X \times \{\emptyset\})$
19		naddcnfid1	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to F {+_{𝑜}}_{f} (X \times \{\emptyset\}) = F$
20	18 19	eqtrd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to (X \times \{\emptyset\}) {+_{𝑜}}_{f} F = F$

Metamath Proof Explorer

Theorem naddcnfid2

Proof