cantnf2

Description: For every ordinal, A , there is a an ordinal exponent b such that A is less than ( _om ^o b ) and for every ordinal at least as large as b there is a unique Cantor normal form, f , with zeros for all the unnecessary higher terms, that sums to A . Theorem 5.3 of Schloeder p. 16. (Contributed by RP, 3-Feb-2025)

		Ref	Expression
	Assertion	cantnf2	$⊢ A \in On \to \exists b \in On \forall c \in (On ∖ b) \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A))$

Proof

Step	Hyp	Ref	Expression
1		onexoegt	$⊢ A \in On \to \exists b \in On A \in (ω ↑_{𝑜} b)$
2		eldif	$⊢ c \in (On ∖ b) \leftrightarrow (c \in On \land \neg c \in b)$
3		simp2	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to b \in On$
4		pm3.2	$⊢ b \in On \to (c \in On \to (b \in On \land c \in On))$
5	3 4	syl	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to (c \in On \to (b \in On \land c \in On))$
6		ontri1	$⊢ (b \in On \land c \in On) \to (b \subseteq c \leftrightarrow \neg c \in b)$
7	5 6	syl6	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to (c \in On \to (b \subseteq c \leftrightarrow \neg c \in b))$
8	7	pm5.32d	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to ((c \in On \land b \subseteq c) \leftrightarrow (c \in On \land \neg c \in b))$
9	2 8	bitr4id	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to (c \in (On ∖ b) \leftrightarrow (c \in On \land b \subseteq c))$
10		simplr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to a = A$
11	10	breq2d	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to (f (ω CNF c) a \leftrightarrow f (ω CNF c) A)$
12		eqid	$⊢ dom (ω CNF c) = dom (ω CNF c)$
13		omelon	$⊢ ω \in On$
14	13	a1i	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to ω \in On$
15		simprl	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to c \in On$
16	15	ad2antrr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to c \in On$
17	12 14 16	cantnff1o	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c$
18		f1ofun	$⊢ (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c \to Fun (ω CNF c)$
19	17 18	syl	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to Fun (ω CNF c)$
20		funbrfvb	$⊢ (Fun (ω CNF c) \land f \in dom (ω CNF c)) \to ((ω CNF c) (f) = A \leftrightarrow f (ω CNF c) A)$
21	19 20	sylancom	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to ((ω CNF c) (f) = A \leftrightarrow f (ω CNF c) A)$
22	11 21	bitr4d	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \land f \in dom (ω CNF c)) \to (f (ω CNF c) a \leftrightarrow (ω CNF c) (f) = A)$
23	22	reubidva	$⊢ (((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land a = A) \to (\exists! f \in dom (ω CNF c) f (ω CNF c) a \leftrightarrow \exists! f \in dom (ω CNF c) (ω CNF c) (f) = A)$
24		simpl2	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to b \in On$
25	13	a1i	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to ω \in On$
26	24 15 25	3jca	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to (b \in On \land c \in On \land ω \in On)$
27		peano1	$⊢ \emptyset \in ω$
28	26 27	jctir	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to ((b \in On \land c \in On \land ω \in On) \land \emptyset \in ω)$
29		simprr	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to b \subseteq c$
30		oewordi	$⊢ ((b \in On \land c \in On \land ω \in On) \land \emptyset \in ω) \to (b \subseteq c \to ω ↑_{𝑜} b \subseteq ω ↑_{𝑜} c)$
31	28 29 30	sylc	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to ω ↑_{𝑜} b \subseteq ω ↑_{𝑜} c$
32		simpl3	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to A \in (ω ↑_{𝑜} b)$
33	31 32	sseldd	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to A \in (ω ↑_{𝑜} c)$
34	12 25 15	cantnff1o	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c$
35		dff1o5	$⊢ (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c \leftrightarrow ((ω CNF c) : dom (ω CNF c) \underset{1-1}{⟶} ω ↑_{𝑜} c \land ran (ω CNF c) = ω ↑_{𝑜} c)$
36		simpr	$⊢ ((ω CNF c) : dom (ω CNF c) \underset{1-1}{⟶} ω ↑_{𝑜} c \land ran (ω CNF c) = ω ↑_{𝑜} c) \to ran (ω CNF c) = ω ↑_{𝑜} c$
37	35 36	sylbi	$⊢ (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c \to ran (ω CNF c) = ω ↑_{𝑜} c$
38	34 37	syl	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to ran (ω CNF c) = ω ↑_{𝑜} c$
39	33 38	eleqtrrd	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to A \in ran (ω CNF c)$
40		dff1o2	$⊢ (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c \leftrightarrow ((ω CNF c) Fn dom (ω CNF c) \land Fun {(ω CNF c)}^{-1} \land ran (ω CNF c) = ω ↑_{𝑜} c)$
41		simp2	$⊢ ((ω CNF c) Fn dom (ω CNF c) \land Fun {(ω CNF c)}^{-1} \land ran (ω CNF c) = ω ↑_{𝑜} c) \to Fun {(ω CNF c)}^{-1}$
42	40 41	sylbi	$⊢ (ω CNF c) : dom (ω CNF c) \underset{1-1 onto}{⟶} ω ↑_{𝑜} c \to Fun {(ω CNF c)}^{-1}$
43	34 42	syl	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to Fun {(ω CNF c)}^{-1}$
44		funcnv3	$⊢ Fun {(ω CNF c)}^{-1} \leftrightarrow \forall a \in ran (ω CNF c) \exists! f \in dom (ω CNF c) f (ω CNF c) a$
45	43 44	sylib	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to \forall a \in ran (ω CNF c) \exists! f \in dom (ω CNF c) f (ω CNF c) a$
46	23 39 45	rspcdv2	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to \exists! f \in dom (ω CNF c) (ω CNF c) (f) = A$
47	32	ad2antrr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to A \in (ω ↑_{𝑜} b)$
48		simplr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to f \in dom (ω CNF c)$
49	13	a1i	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to ω \in On$
50	15	ad2antrr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to c \in On$
51	12 49 50	cantnfs	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (f \in dom (ω CNF c) \leftrightarrow (f : c ⟶ ω \land {finSupp}_{\emptyset} (f)))$
52	48 51	mpbid	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (f : c ⟶ ω \land {finSupp}_{\emptyset} (f))$
53		simpr	$⊢ (f : c ⟶ ω \land {finSupp}_{\emptyset} (f)) \to {finSupp}_{\emptyset} (f)$
54	52 53	syl	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to {finSupp}_{\emptyset} (f)$
55		eqid	$⊢ dom (ω CNF b) = dom (ω CNF b)$
56	24	ad2antrr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to b \in On$
57	29	ad2antrr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to b \subseteq c$
58		simpr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF c) (f) = A$
59	58 47	eqeltrd	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF c) (f) \in (ω ↑_{𝑜} b)$
60		1onn	$⊢ 1_{𝑜} \in ω$
61		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
62	13 60 61	mpbir2an	$⊢ ω \in (On ∖ 2_{𝑜})$
63	62	a1i	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to ω \in (On ∖ 2_{𝑜})$
64		cantnfresb	$⊢ ((ω \in (On ∖ 2_{𝑜}) \land c \in On) \land (b \in On \land f \in dom (ω CNF c))) \to ((ω CNF c) (f) \in (ω ↑_{𝑜} b) \leftrightarrow \forall d \in (c ∖ b) f (d) = \emptyset)$
65	63 50 56 48 64	syl22anc	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to ((ω CNF c) (f) \in (ω ↑_{𝑜} b) \leftrightarrow \forall d \in (c ∖ b) f (d) = \emptyset)$
66	59 65	mpbid	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to \forall d \in (c ∖ b) f (d) = \emptyset$
67	66	r19.21bi	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in (c ∖ b)) \to f (d) = \emptyset$
68	27	a1i	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to \emptyset \in ω$
69		simpllr	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to f \in dom (ω CNF c)$
70	13	a1i	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to ω \in On$
71	15	adantr	$⊢ (((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \to c \in On$
72	71	ad2antrr	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to c \in On$
73	12 70 72	cantnfs	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to (f \in dom (ω CNF c) \leftrightarrow (f : c ⟶ ω \land {finSupp}_{\emptyset} (f)))$
74	69 73	mpbid	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to (f : c ⟶ ω \land {finSupp}_{\emptyset} (f))$
75	74	simpld	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to f : c ⟶ ω$
76	57	sselda	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to d \in c$
77	75 76	ffvelcdmd	$⊢ (((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \land d \in b) \to f (d) \in ω$
78	77	fmpttd	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (d \in b ⟼ f (d)) : b ⟶ ω$
79	12 25 15	cantnfs	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to (f \in dom (ω CNF c) \leftrightarrow (f : c ⟶ ω \land {finSupp}_{\emptyset} (f)))$
80	79	simprbda	$⊢ (((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \to f : c ⟶ ω$
81	80	adantr	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to f : c ⟶ ω$
82	81 57	feqresmpt	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to {f ↾}_{b} = (d \in b ⟼ f (d))$
83	54 68	fsuppres	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to {finSupp}_{\emptyset} (({f ↾}_{b}))$
84	82 83	eqbrtrrd	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to {finSupp}_{\emptyset} ((d \in b ⟼ f (d)))$
85	55 49 56	cantnfs	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to ((d \in b ⟼ f (d)) \in dom (ω CNF b) \leftrightarrow ((d \in b ⟼ f (d)) : b ⟶ ω \land {finSupp}_{\emptyset} ((d \in b ⟼ f (d)))))$
86	78 84 85	mpbir2and	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (d \in b ⟼ f (d)) \in dom (ω CNF b)$
87	55 49 56 50 57 67 68 12 86	cantnfres	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF b) ((d \in b ⟼ f (d))) = (ω CNF c) ((d \in c ⟼ f (d)))$
88	82	fveq2d	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF b) ({f ↾}_{b}) = (ω CNF b) ((d \in b ⟼ f (d)))$
89	81	feqmptd	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to f = (d \in c ⟼ f (d))$
90	89	fveq2d	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF c) (f) = (ω CNF c) ((d \in c ⟼ f (d)))$
91	87 88 90	3eqtr4d	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF b) ({f ↾}_{b}) = (ω CNF c) (f)$
92	91 58	eqtrd	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (ω CNF b) ({f ↾}_{b}) = A$
93	47 54 92	3jca	$⊢ ((((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \land (ω CNF c) (f) = A) \to (A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f) \land (ω CNF b) ({f ↾}_{b}) = A)$
94	93	ex	$⊢ (((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \to ((ω CNF c) (f) = A \to (A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f) \land (ω CNF b) ({f ↾}_{b}) = A))$
95	94	pm4.71rd	$⊢ (((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \to ((ω CNF c) (f) = A \leftrightarrow ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f) \land (ω CNF b) ({f ↾}_{b}) = A) \land (ω CNF c) (f) = A))$
96		3an4anass	$⊢ ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f) \land (ω CNF b) ({f ↾}_{b}) = A) \land (ω CNF c) (f) = A) \leftrightarrow ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A))$
97	95 96	bitrdi	$⊢ (((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \land f \in dom (ω CNF c)) \to ((ω CNF c) (f) = A \leftrightarrow ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A)))$
98	97	reubidva	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to (\exists! f \in dom (ω CNF c) (ω CNF c) (f) = A \leftrightarrow \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A)))$
99	46 98	mpbid	$⊢ ((A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \land (c \in On \land b \subseteq c)) \to \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A))$
100	99	ex	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to ((c \in On \land b \subseteq c) \to \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A)))$
101	9 100	sylbid	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to (c \in (On ∖ b) \to \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A)))$
102	101	ralrimiv	$⊢ (A \in On \land b \in On \land A \in (ω ↑_{𝑜} b)) \to \forall c \in (On ∖ b) \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A))$
103	102	3exp	$⊢ A \in On \to (b \in On \to (A \in (ω ↑_{𝑜} b) \to \forall c \in (On ∖ b) \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A))))$
104	103	reximdvai	$⊢ A \in On \to (\exists b \in On A \in (ω ↑_{𝑜} b) \to \exists b \in On \forall c \in (On ∖ b) \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A)))$
105	1 104	mpd	$⊢ A \in On \to \exists b \in On \forall c \in (On ∖ b) \exists! f \in dom (ω CNF c) ((A \in (ω ↑_{𝑜} b) \land {finSupp}_{\emptyset} (f)) \land ((ω CNF b) ({f ↾}_{b}) = A \land (ω CNF c) (f) = A))$

Metamath Proof Explorer

Theorem cantnf2

Proof