naddcnfcom

Description: Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (X \in On \land S = dom (ω CNF X)) \to S = dom (ω CNF X)$
2	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \leftrightarrow F \in dom (ω CNF X))$
3		eqid	$⊢ dom (ω CNF X) = dom (ω CNF X)$
4		omelon	$⊢ ω \in On$
5	4	a1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to ω \in On$
6		simpl	$⊢ (X \in On \land S = dom (ω CNF X)) \to X \in On$
7	3 5 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in dom (ω CNF X) \leftrightarrow (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)))$
8	2 7	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \leftrightarrow (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)))$
9		simpl	$⊢ (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)) \to F : X ⟶ ω$
10	8 9	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \to F : X ⟶ ω)$
11		simpl	$⊢ (F \in S \land G \in S) \to F \in S$
12	10 11	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F : X ⟶ ω$
13	12	ffnd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F Fn X$
14	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \leftrightarrow G \in dom (ω CNF X))$
15	3 5 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in dom (ω CNF X) \leftrightarrow (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)))$
16	14 15	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \leftrightarrow (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)))$
17		simpl	$⊢ (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)) \to G : X ⟶ ω$
18	16 17	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \to G : X ⟶ ω)$
19		simpr	$⊢ (F \in S \land G \in S) \to G \in S$
20	18 19	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to G : X ⟶ ω$
21	20	ffnd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to G Fn X$
22		simpll	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to X \in On$
23		inidm	$⊢ X \cap X = X$
24	13 21 22 22 23	offn	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to (F {+_{𝑜}}_{f} G) Fn X$
25	21 13 22 22 23	offn	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to (G {+_{𝑜}}_{f} F) Fn X$
26	12	ffvelcdmda	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to F (x) \in ω$
27	20	ffvelcdmda	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to G (x) \in ω$
28		nnacom	$⊢ (F (x) \in ω \land G (x) \in ω) \to F (x) +_{𝑜} G (x) = G (x) +_{𝑜} F (x)$
29	26 27 28	syl2anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to F (x) +_{𝑜} G (x) = G (x) +_{𝑜} F (x)$
30	13	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to F Fn X$
31	21	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to G Fn X$
32		simplll	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to X \in On$
33		simpr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to x \in X$
34		fnfvof	$⊢ ((F Fn X \land G Fn X) \land (X \in On \land x \in X)) \to (F {+_{𝑜}}_{f} G) (x) = F (x) +_{𝑜} G (x)$
35	30 31 32 33 34	syl22anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} G) (x) = F (x) +_{𝑜} G (x)$
36		fnfvof	$⊢ ((G Fn X \land F Fn X) \land (X \in On \land x \in X)) \to (G {+_{𝑜}}_{f} F) (x) = G (x) +_{𝑜} F (x)$
37	31 30 32 33 36	syl22anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to (G {+_{𝑜}}_{f} F) (x) = G (x) +_{𝑜} F (x)$
38	29 35 37	3eqtr4d	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} G) (x) = (G {+_{𝑜}}_{f} F) (x)$
39	24 25 38	eqfnfvd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F {+_{𝑜}}_{f} G = G {+_{𝑜}}_{f} F$

Metamath Proof Explorer

Theorem naddcnfcom

Proof