naddcnffo

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

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

Proof

Step	Hyp	Ref	Expression
1		naddcnff	$⊢ (X \in On \land S = dom (ω CNF X)) \to ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S ⟶ S$
2		simpr	$⊢ ((X \in On \land S = dom (ω CNF X)) \land f \in S) \to f \in S$
3		peano1	$⊢ \emptyset \in ω$
4		fconst6g	$⊢ \emptyset \in ω \to (X \times \{\emptyset\}) : X ⟶ ω$
5	3 4	mp1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to (X \times \{\emptyset\}) : X ⟶ ω$
6		simpl	$⊢ (X \in On \land S = dom (ω CNF X)) \to X \in On$
7	3	a1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to \emptyset \in ω$
8	6 7	fczfsuppd	$⊢ (X \in On \land S = dom (ω CNF X)) \to {finSupp}_{\emptyset} ((X \times \{\emptyset\}))$
9		simpr	$⊢ (X \in On \land S = dom (ω CNF X)) \to S = dom (ω CNF X)$
10	9	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (X \times \{\emptyset\} \in S \leftrightarrow X \times \{\emptyset\} \in dom (ω CNF X))$
11		eqid	$⊢ dom (ω CNF X) = dom (ω CNF X)$
12		omelon	$⊢ ω \in On$
13	12	a1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to ω \in On$
14	11 13 6	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\}))))$
15	10 14	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\}))))$
16	5 8 15	mpbir2and	$⊢ (X \in On \land S = dom (ω CNF X)) \to X \times \{\emptyset\} \in S$
17	16	adantr	$⊢ ((X \in On \land S = dom (ω CNF X)) \land f \in S) \to X \times \{\emptyset\} \in S$
18		simpl	$⊢ (f \in S \land X \times \{\emptyset\} \in S) \to f \in S$
19	18	adantl	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to f \in S$
20		simpr	$⊢ (f \in S \land X \times \{\emptyset\} \in S) \to X \times \{\emptyset\} \in S$
21	20	adantl	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to X \times \{\emptyset\} \in S$
22	19 21	ovresd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) (X \times \{\emptyset\}) = f {+_{𝑜}}_{f} (X \times \{\emptyset\})$
23	9	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f \in S \leftrightarrow f \in dom (ω CNF X))$
24	11 13 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f \in dom (ω CNF X) \leftrightarrow (f : X ⟶ ω \land {finSupp}_{\emptyset} (f)))$
25	23 24	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f \in S \leftrightarrow (f : X ⟶ ω \land {finSupp}_{\emptyset} (f)))$
26	25	biimpd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (f \in S \to (f : X ⟶ ω \land {finSupp}_{\emptyset} (f)))$
27		simpl	$⊢ (f : X ⟶ ω \land {finSupp}_{\emptyset} (f)) \to f : X ⟶ ω$
28	18 26 27	syl56	$⊢ (X \in On \land S = dom (ω CNF X)) \to ((f \in S \land X \times \{\emptyset\} \in S) \to f : X ⟶ ω)$
29	28	imp	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to f : X ⟶ ω$
30	29	ffnd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to f Fn X$
31		fnconstg	$⊢ \emptyset \in ω \to (X \times \{\emptyset\}) Fn X$
32	3 31	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$
33	6	adantr	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to X \in On$
34		inidm	$⊢ X \cap X = X$
35	30 32 33 33 34	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$
36	30	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$
37	3 31	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$
38		simplll	$⊢ (((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$
39		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$
40		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)$
41	36 37 38 39 40	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)$
42	3	a1i	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \land x \in X) \to \emptyset \in ω$
43		fvconst2g	$⊢ (\emptyset \in ω \land x \in X) \to (X \times \{\emptyset\}) (x) = \emptyset$
44	42 39 43	syl2anc	$⊢ (((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$
45	44	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$
46	29	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 ω$
47		nnon	$⊢ f (x) \in ω \to f (x) \in On$
48		oa0	$⊢ f (x) \in On \to f (x) +_{𝑜} \emptyset = f (x)$
49	46 47 48	3syl	$⊢ (((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)$
50	41 45 49	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)$
51	35 30 50	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$
52	22 51	eqtr2d	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (f \in S \land X \times \{\emptyset\} \in S)) \to f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) (X \times \{\emptyset\})$
53	52	expr	$⊢ ((X \in On \land S = dom (ω CNF X)) \land f \in S) \to (X \times \{\emptyset\} \in S \to f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) (X \times \{\emptyset\}))$
54	17 53	jcai	$⊢ ((X \in On \land S = dom (ω CNF X)) \land f \in S) \to (X \times \{\emptyset\} \in S \land f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) (X \times \{\emptyset\}))$
55		oveq2	$⊢ z = X \times \{\emptyset\} \to f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) (X \times \{\emptyset\})$
56	55	rspceeqv	$⊢ (X \times \{\emptyset\} \in S \land f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) (X \times \{\emptyset\})) \to \exists z \in S f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z$
57	54 56	syl	$⊢ ((X \in On \land S = dom (ω CNF X)) \land f \in S) \to \exists z \in S f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z$
58		oveq1	$⊢ g = f \to g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z$
59	58	eqeq2d	$⊢ g = f \to (f = g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z \leftrightarrow f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z)$
60	59	rexbidv	$⊢ g = f \to (\exists z \in S f = g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z \leftrightarrow \exists z \in S f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z)$
61	60	rspcev	$⊢ (f \in S \land \exists z \in S f = f ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z) \to \exists g \in S \exists z \in S f = g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z$
62	2 57 61	syl2anc	$⊢ ((X \in On \land S = dom (ω CNF X)) \land f \in S) \to \exists g \in S \exists z \in S f = g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z$
63	62	ralrimiva	$⊢ (X \in On \land S = dom (ω CNF X)) \to \forall f \in S \exists g \in S \exists z \in S f = g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z$
64		foov	$⊢ ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S \underset{onto}{⟶} S \leftrightarrow (({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S ⟶ S \land \forall f \in S \exists g \in S \exists z \in S f = g ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) z)$
65	1 63 64	sylanbrc	$⊢ (X \in On \land S = dom (ω CNF X)) \to ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S \underset{onto}{⟶} S$

Metamath Proof Explorer

Theorem naddcnffo

Proof