naddcnfid1

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

		Ref	Expression
	Assertion	naddcnfid1	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to F {+_{𝑜}}_{f} (X \times \{\emptyset\}) = 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	7	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \leftrightarrow F \in dom (ω CNF X))$
16	9 11 4	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in dom (ω CNF X) \leftrightarrow (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)))$
17	15 16	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \leftrightarrow (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)))$
18	17	simprbda	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to F : X ⟶ ω$
19	18	ffnd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to F Fn X$
20	19	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \to F Fn X$
21	2	ffnd	$⊢ \emptyset \in ω \to (X \times \{\emptyset\}) Fn X$
22	1 21	mp1i	$⊢ (((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \to (X \times \{\emptyset\}) Fn X$
23		simplll	$⊢ (((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \to X \in On$
24		inidm	$⊢ X \cap X = X$
25	20 22 23 23 24	offn	$⊢ (((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \to (F {+_{𝑜}}_{f} (X \times \{\emptyset\})) Fn X$
26	20	adantr	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to F Fn X$
27	1 21	mp1i	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to (X \times \{\emptyset\}) Fn X$
28		simp-4l	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to X \in On$
29		simpr	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to x \in X$
30		fnfvof	$⊢ ((F Fn X \land (X \times \{\emptyset\}) Fn X) \land (X \in On \land x \in X)) \to (F {+_{𝑜}}_{f} (X \times \{\emptyset\})) (x) = F (x) +_{𝑜} (X \times \{\emptyset\}) (x)$
31	26 27 28 29 30	syl22anc	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to (F {+_{𝑜}}_{f} (X \times \{\emptyset\})) (x) = F (x) +_{𝑜} (X \times \{\emptyset\}) (x)$
32		fvconst2g	$⊢ (\emptyset \in ω \land x \in X) \to (X \times \{\emptyset\}) (x) = \emptyset$
33	1 29 32	sylancr	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to (X \times \{\emptyset\}) (x) = \emptyset$
34	33	oveq2d	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to F (x) +_{𝑜} (X \times \{\emptyset\}) (x) = F (x) +_{𝑜} \emptyset$
35	18	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \to F : X ⟶ ω$
36	35	ffvelcdmda	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to F (x) \in ω$
37		nna0	$⊢ F (x) \in ω \to F (x) +_{𝑜} \emptyset = F (x)$
38	36 37	syl	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to F (x) +_{𝑜} \emptyset = F (x)$
39	31 34 38	3eqtrd	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \land x \in X) \to (F {+_{𝑜}}_{f} (X \times \{\emptyset\})) (x) = F (x)$
40	25 20 39	eqfnfvd	$⊢ (((X \in On \land S = dom (ω CNF X)) \land F \in S) \land X \times \{\emptyset\} \in S) \to F {+_{𝑜}}_{f} (X \times \{\emptyset\}) = F$
41	14 40	mpidan	$⊢ ((X \in On \land S = dom (ω CNF X)) \land F \in S) \to F {+_{𝑜}}_{f} (X \times \{\emptyset\}) = F$

Metamath Proof Explorer

Theorem naddcnfid1

Proof