naddcnff

Description: Addition operator for Cantor normal forms is a function into Cantor normal forms. (Contributed by RP, 2-Jan-2025)

		Ref	Expression
	Assertion	naddcnff	$⊢ (X \in On \land S = dom (ω CNF X)) \to ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S ⟶ S$

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	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (g \in S \leftrightarrow g \in dom (ω CNF X))$
10	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)))$
11	9 10	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (g \in S \leftrightarrow (g : X ⟶ ω \land {finSupp}_{\emptyset} (g)))$
12	11	adantr	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \to (g \in S \leftrightarrow (g : X ⟶ ω \land {finSupp}_{\emptyset} (g)))$
13		simpl	$⊢ (f : X ⟶ ω \land {finSupp}_{\emptyset} (f)) \to f : X ⟶ ω$
14		simpl	$⊢ (g : X ⟶ ω \land {finSupp}_{\emptyset} (g)) \to g : X ⟶ ω$
15	13 14	anim12i	$⊢ ((f : X ⟶ ω \land {finSupp}_{\emptyset} (f)) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to (f : X ⟶ ω \land g : X ⟶ ω)$
16	6 15	anim12i	$⊢ ((X \in On \land S = dom (ω CNF X)) \land ((f : X ⟶ ω \land {finSupp}_{\emptyset} (f)) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g)))) \to (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω))$
17	16	anassrs	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω))$
18		simprl	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to f : X ⟶ ω$
19	18	ffnd	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to f Fn X$
20		simprr	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to g : X ⟶ ω$
21	20	ffnd	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to g Fn X$
22		simpl	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to X \in On$
23		inidm	$⊢ X \cap X = X$
24	19 21 22 22 23	offn	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to (f {+_{𝑜}}_{f} g) Fn X$
25		simpr	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land (f {+_{𝑜}}_{f} g) Fn X) \to (f {+_{𝑜}}_{f} g) Fn X$
26		simplrl	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to f : X ⟶ ω$
27	26	ffnd	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to f Fn X$
28		simplrr	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to g : X ⟶ ω$
29	28	ffnd	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to g Fn X$
30		simpll	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to X \in On$
31		simpr	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to x \in X$
32		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)$
33	27 29 30 31 32	syl22anc	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to (f {+_{𝑜}}_{f} g) (x) = f (x) +_{𝑜} g (x)$
34	18	ffvelcdmda	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to f (x) \in ω$
35	20	ffvelcdmda	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to g (x) \in ω$
36		nnacl	$⊢ (f (x) \in ω \land g (x) \in ω) \to f (x) +_{𝑜} g (x) \in ω$
37	34 35 36	syl2anc	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to f (x) +_{𝑜} g (x) \in ω$
38	33 37	eqeltrd	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land x \in X) \to (f {+_{𝑜}}_{f} g) (x) \in ω$
39	38	ex	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to (x \in X \to (f {+_{𝑜}}_{f} g) (x) \in ω)$
40	39	ralrimiv	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to \forall x \in X (f {+_{𝑜}}_{f} g) (x) \in ω$
41	40	adantr	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land (f {+_{𝑜}}_{f} g) Fn X) \to \forall x \in X (f {+_{𝑜}}_{f} g) (x) \in ω$
42		fnfvrnss	$⊢ ((f {+_{𝑜}}_{f} g) Fn X \land \forall x \in X (f {+_{𝑜}}_{f} g) (x) \in ω) \to ran (f {+_{𝑜}}_{f} g) \subseteq ω$
43	25 41 42	syl2anc	$⊢ ((X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \land (f {+_{𝑜}}_{f} g) Fn X) \to ran (f {+_{𝑜}}_{f} g) \subseteq ω$
44	43	ex	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to ((f {+_{𝑜}}_{f} g) Fn X \to ran (f {+_{𝑜}}_{f} g) \subseteq ω)$
45	24 44	jcai	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to ((f {+_{𝑜}}_{f} g) Fn X \land ran (f {+_{𝑜}}_{f} g) \subseteq ω)$
46		df-f	$⊢ (f {+_{𝑜}}_{f} g) : X ⟶ ω \leftrightarrow ((f {+_{𝑜}}_{f} g) Fn X \land ran (f {+_{𝑜}}_{f} g) \subseteq ω)$
47	45 46	sylibr	$⊢ (X \in On \land (f : X ⟶ ω \land g : X ⟶ ω)) \to (f {+_{𝑜}}_{f} g) : X ⟶ ω$
48	17 47	syl	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to (f {+_{𝑜}}_{f} g) : X ⟶ ω$
49		ffun	$⊢ (f {+_{𝑜}}_{f} g) : X ⟶ ω \to Fun (f {+_{𝑜}}_{f} g)$
50	49	adantl	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to Fun (f {+_{𝑜}}_{f} g)$
51		simplrr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to {finSupp}_{\emptyset} (f)$
52	51	adantr	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to {finSupp}_{\emptyset} (f)$
53		simplrr	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to {finSupp}_{\emptyset} (g)$
54	52 53	fsuppunfi	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to {supp}_{\emptyset} (f) \cup {supp}_{\emptyset} (g) \in Fin$
55		simp-4l	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to X \in On$
56		peano1	$⊢ \emptyset \in ω$
57	56	a1i	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to \emptyset \in ω$
58		simplrl	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to f : X ⟶ ω$
59	58	adantr	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to f : X ⟶ ω$
60		simplrl	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to g : X ⟶ ω$
61		0elon	$⊢ \emptyset \in On$
62		oa0	$⊢ \emptyset \in On \to \emptyset +_{𝑜} \emptyset = \emptyset$
63	61 62	mp1i	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to \emptyset +_{𝑜} \emptyset = \emptyset$
64	55 57 59 60 63	suppofssd	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to (f {+_{𝑜}}_{f} g) supp \emptyset \subseteq {supp}_{\emptyset} (f) \cup {supp}_{\emptyset} (g)$
65	54 64	ssfid	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to (f {+_{𝑜}}_{f} g) supp \emptyset \in Fin$
66		ovexd	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to f {+_{𝑜}}_{f} g \in V$
67		isfsupp	$⊢ (f {+_{𝑜}}_{f} g \in V \land \emptyset \in On) \to ({finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g)) \leftrightarrow (Fun (f {+_{𝑜}}_{f} g) \land (f {+_{𝑜}}_{f} g) supp \emptyset \in Fin))$
68	66 61 67	sylancl	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to ({finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g)) \leftrightarrow (Fun (f {+_{𝑜}}_{f} g) \land (f {+_{𝑜}}_{f} g) supp \emptyset \in Fin))$
69	50 65 68	mpbir2and	$⊢ ((((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \land (f {+_{𝑜}}_{f} g) : X ⟶ ω) \to {finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g))$
70	69	ex	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to ((f {+_{𝑜}}_{f} g) : X ⟶ ω \to {finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g)))$
71	48 70	jcai	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to ((f {+_{𝑜}}_{f} g) : X ⟶ ω \land {finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g)))$
72	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f {+_{𝑜}}_{f} g \in S \leftrightarrow f {+_{𝑜}}_{f} g \in dom (ω CNF X))$
73	3 5 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f {+_{𝑜}}_{f} g \in dom (ω CNF X) \leftrightarrow ((f {+_{𝑜}}_{f} g) : X ⟶ ω \land {finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g))))$
74	72 73	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f {+_{𝑜}}_{f} g \in S \leftrightarrow ((f {+_{𝑜}}_{f} g) : X ⟶ ω \land {finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g))))$
75	74	ad2antrr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to (f {+_{𝑜}}_{f} g \in S \leftrightarrow ((f {+_{𝑜}}_{f} g) : X ⟶ ω \land {finSupp}_{\emptyset} ((f {+_{𝑜}}_{f} g))))$
76	71 75	mpbird	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \land (g : X ⟶ ω \land {finSupp}_{\emptyset} (g))) \to f {+_{𝑜}}_{f} g \in S$
77	76	ex	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \to ((g : X ⟶ ω \land {finSupp}_{\emptyset} (g)) \to f {+_{𝑜}}_{f} g \in S)$
78	12 77	sylbid	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \to (g \in S \to f {+_{𝑜}}_{f} g \in S)$
79	78	ralrimiv	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f : X ⟶ ω \land {finSupp}_{\emptyset} (f))) \to \forall g \in S f {+_{𝑜}}_{f} g \in S$
80	79	ex	$⊢ (X \in On \land S = dom (ω CNF X)) \to ((f : X ⟶ ω \land {finSupp}_{\emptyset} (f)) \to \forall g \in S f {+_{𝑜}}_{f} g \in S)$
81	8 80	sylbid	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f \in S \to \forall g \in S f {+_{𝑜}}_{f} g \in S)$
82	81	ralrimiv	$⊢ (X \in On \land S = dom (ω CNF X)) \to \forall f \in S \forall g \in S f {+_{𝑜}}_{f} g \in S$
83		ofmres	$⊢ {\circ_{f} +_{𝑜} ↾}_{(S \times S)} = (f \in S, g \in S ⟼ f {+_{𝑜}}_{f} g)$
84	83	fmpo	$⊢ \forall f \in S \forall g \in S f {+_{𝑜}}_{f} g \in S \leftrightarrow ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S ⟶ S$
85	82 84	sylib	$⊢ (X \in On \land S = dom (ω CNF X)) \to ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S ⟶ S$

Metamath Proof Explorer

Theorem naddcnff

Proof