cantnff

Description: The CNF function is a function from finitely supported functions from B to A , to the ordinal exponential A ^o B . (Contributed by Mario Carneiro, 28-May-2015)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
Assertion	cantnff	$⊢ φ \to (A CNF B) : S ⟶ A ↑_{𝑜} B$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		fvex	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) \in V$
5	4	csbex	$⊢ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) \in V$
6	5	a1i	$⊢ (φ \land f \in S) \to ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) \in V$
7		eqid	$⊢ \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
8	7 2 3	cantnffval	$⊢ φ \to A CNF B = (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
9	7 2 3	cantnfdm	$⊢ φ \to dom (A CNF B) = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
10	1 9	syl5eq	$⊢ φ \to S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
11	10	mpteq1d	$⊢ φ \to (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) = (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
12	8 11	eqtr4d	$⊢ φ \to A CNF B = (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
13	2	adantr	$⊢ (φ \land x \in S) \to A \in On$
14	3	adantr	$⊢ (φ \land x \in S) \to B \in On$
15		eqid	$⊢ OrdIso (E, x supp \emptyset) = OrdIso (E, x supp \emptyset)$
16		simpr	$⊢ (φ \land x \in S) \to x \in S$
17		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
18	1 13 14 15 16 17	cantnfval	$⊢ (φ \land x \in S) \to (A CNF B) (x) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, x supp \emptyset))$
19	18	adantr	$⊢ ((φ \land x \in S) \land A = \emptyset) \to (A CNF B) (x) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, x supp \emptyset))$
20		ovex	$⊢ x supp \emptyset \in V$
21	1 13 14 15 16	cantnfcl	$⊢ (φ \land x \in S) \to (E We {supp}_{\emptyset} (x) \land dom OrdIso (E, x supp \emptyset) \in ω)$
22	21	simpld	$⊢ (φ \land x \in S) \to E We {supp}_{\emptyset} (x)$
23	15	oien	$⊢ (x supp \emptyset \in V \land E We {supp}_{\emptyset} (x)) \to dom OrdIso (E, x supp \emptyset) \approx {supp}_{\emptyset} (x)$
24	20 22 23	sylancr	$⊢ (φ \land x \in S) \to dom OrdIso (E, x supp \emptyset) \approx {supp}_{\emptyset} (x)$
25	24	adantr	$⊢ ((φ \land x \in S) \land A = \emptyset) \to dom OrdIso (E, x supp \emptyset) \approx {supp}_{\emptyset} (x)$
26		suppssdm	$⊢ x supp \emptyset \subseteq dom x$
27	1 2 3	cantnfs	$⊢ φ \to (x \in S \leftrightarrow (x : B ⟶ A \land {finSupp}_{\emptyset} (x)))$
28	27	simprbda	$⊢ (φ \land x \in S) \to x : B ⟶ A$
29	26 28	fssdm	$⊢ (φ \land x \in S) \to x supp \emptyset \subseteq B$
30		feq3	$⊢ A = \emptyset \to (x : B ⟶ A \leftrightarrow x : B ⟶ \emptyset)$
31	28 30	syl5ibcom	$⊢ (φ \land x \in S) \to (A = \emptyset \to x : B ⟶ \emptyset)$
32	31	imp	$⊢ ((φ \land x \in S) \land A = \emptyset) \to x : B ⟶ \emptyset$
33		f00	$⊢ x : B ⟶ \emptyset \leftrightarrow (x = \emptyset \land B = \emptyset)$
34	32 33	sylib	$⊢ ((φ \land x \in S) \land A = \emptyset) \to (x = \emptyset \land B = \emptyset)$
35	34	simprd	$⊢ ((φ \land x \in S) \land A = \emptyset) \to B = \emptyset$
36		sseq0	$⊢ (x supp \emptyset \subseteq B \land B = \emptyset) \to x supp \emptyset = \emptyset$
37	29 35 36	syl2an2r	$⊢ ((φ \land x \in S) \land A = \emptyset) \to x supp \emptyset = \emptyset$
38	25 37	breqtrd	$⊢ ((φ \land x \in S) \land A = \emptyset) \to dom OrdIso (E, x supp \emptyset) \approx \emptyset$
39		en0	$⊢ dom OrdIso (E, x supp \emptyset) \approx \emptyset \leftrightarrow dom OrdIso (E, x supp \emptyset) = \emptyset$
40	38 39	sylib	$⊢ ((φ \land x \in S) \land A = \emptyset) \to dom OrdIso (E, x supp \emptyset) = \emptyset$
41	40	fveq2d	$⊢ ((φ \land x \in S) \land A = \emptyset) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, x supp \emptyset)) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) (\emptyset)$
42		0ex	$⊢ \emptyset \in V$
43	17	seqom0g	$⊢ \emptyset \in V \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) (\emptyset) = \emptyset$
44	42 43	mp1i	$⊢ ((φ \land x \in S) \land A = \emptyset) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, x supp \emptyset) (k)) \cdot_{𝑜} x (OrdIso (E, x supp \emptyset) (k))) +_{𝑜} z), \emptyset) (\emptyset) = \emptyset$
45	19 41 44	3eqtrd	$⊢ ((φ \land x \in S) \land A = \emptyset) \to (A CNF B) (x) = \emptyset$
46		el1o	$⊢ (A CNF B) (x) \in 1_{𝑜} \leftrightarrow (A CNF B) (x) = \emptyset$
47	45 46	sylibr	$⊢ ((φ \land x \in S) \land A = \emptyset) \to (A CNF B) (x) \in 1_{𝑜}$
48	35	oveq2d	$⊢ ((φ \land x \in S) \land A = \emptyset) \to A ↑_{𝑜} B = A ↑_{𝑜} \emptyset$
49	13	adantr	$⊢ ((φ \land x \in S) \land A = \emptyset) \to A \in On$
50		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
51	49 50	syl	$⊢ ((φ \land x \in S) \land A = \emptyset) \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
52	48 51	eqtrd	$⊢ ((φ \land x \in S) \land A = \emptyset) \to A ↑_{𝑜} B = 1_{𝑜}$
53	47 52	eleqtrrd	$⊢ ((φ \land x \in S) \land A = \emptyset) \to (A CNF B) (x) \in (A ↑_{𝑜} B)$
54	13	adantr	$⊢ ((φ \land x \in S) \land A \neq \emptyset) \to A \in On$
55	14	adantr	$⊢ ((φ \land x \in S) \land A \neq \emptyset) \to B \in On$
56	16	adantr	$⊢ ((φ \land x \in S) \land A \neq \emptyset) \to x \in S$
57		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
58	13 57	syl	$⊢ (φ \land x \in S) \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
59	58	biimpar	$⊢ ((φ \land x \in S) \land A \neq \emptyset) \to \emptyset \in A$
60	29	adantr	$⊢ ((φ \land x \in S) \land A \neq \emptyset) \to x supp \emptyset \subseteq B$
61	1 54 55 56 59 55 60	cantnflt2	$⊢ ((φ \land x \in S) \land A \neq \emptyset) \to (A CNF B) (x) \in (A ↑_{𝑜} B)$
62	53 61	pm2.61dane	$⊢ (φ \land x \in S) \to (A CNF B) (x) \in (A ↑_{𝑜} B)$
63	6 12 62	fmpt2d	$⊢ φ \to (A CNF B) : S ⟶ A ↑_{𝑜} B$

Metamath Proof Explorer

Theorem cantnff

Proof