cantnfp1

Description: If F is created by adding a single term ( FX ) = Y to G , where X is larger than any element of the support of G , then F is also a finitely supported function and it is assigned the value ( ( A ^o X ) .o Y ) +o z where z is the value of G . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 1-Jul-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfp1.g	$⊢ φ \to G \in S$
	cantnfp1.x	$⊢ φ \to X \in B$
	cantnfp1.y	$⊢ φ \to Y \in A$
	cantnfp1.s	$⊢ φ \to G supp \emptyset \subseteq X$
	cantnfp1.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
Assertion	cantnfp1	$⊢ φ \to (F \in S \land (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G))$

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		cantnfp1.g	$⊢ φ \to G \in S$
5		cantnfp1.x	$⊢ φ \to X \in B$
6		cantnfp1.y	$⊢ φ \to Y \in A$
7		cantnfp1.s	$⊢ φ \to G supp \emptyset \subseteq X$
8		cantnfp1.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
9		onelon	$⊢ (B \in On \land X \in B) \to X \in On$
10	3 5 9	syl2anc	$⊢ φ \to X \in On$
11		eloni	$⊢ X \in On \to Ord X$
12		ordirr	$⊢ Ord X \to \neg X \in X$
13	10 11 12	3syl	$⊢ φ \to \neg X \in X$
14		fvex	$⊢ G (X) \in V$
15		dif1o	$⊢ G (X) \in (V ∖ 1_{𝑜}) \leftrightarrow (G (X) \in V \land G (X) \neq \emptyset)$
16	14 15	mpbiran	$⊢ G (X) \in (V ∖ 1_{𝑜}) \leftrightarrow G (X) \neq \emptyset$
17	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
18	4 17	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
19	18	simpld	$⊢ φ \to G : B ⟶ A$
20	19	ffnd	$⊢ φ \to G Fn B$
21		0ex	$⊢ \emptyset \in V$
22	21	a1i	$⊢ φ \to \emptyset \in V$
23		elsuppfn	$⊢ (G Fn B \land B \in On \land \emptyset \in V) \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
24	20 3 22 23	syl3anc	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
25	16	bicomi	$⊢ G (X) \neq \emptyset \leftrightarrow G (X) \in (V ∖ 1_{𝑜})$
26	25	a1i	$⊢ φ \to (G (X) \neq \emptyset \leftrightarrow G (X) \in (V ∖ 1_{𝑜}))$
27	26	anbi2d	$⊢ φ \to ((X \in B \land G (X) \neq \emptyset) \leftrightarrow (X \in B \land G (X) \in (V ∖ 1_{𝑜})))$
28	24 27	bitrd	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \in (V ∖ 1_{𝑜})))$
29	7	sseld	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \to X \in X)$
30	28 29	sylbird	$⊢ φ \to ((X \in B \land G (X) \in (V ∖ 1_{𝑜})) \to X \in X)$
31	5 30	mpand	$⊢ φ \to (G (X) \in (V ∖ 1_{𝑜}) \to X \in X)$
32	16 31	syl5bir	$⊢ φ \to (G (X) \neq \emptyset \to X \in X)$
33	32	necon1bd	$⊢ φ \to (\neg X \in X \to G (X) = \emptyset)$
34	13 33	mpd	$⊢ φ \to G (X) = \emptyset$
35	34	ad3antrrr	$⊢ (((φ \land Y = \emptyset) \land t \in B) \land t = X) \to G (X) = \emptyset$
36		simpr	$⊢ (((φ \land Y = \emptyset) \land t \in B) \land t = X) \to t = X$
37	36	fveq2d	$⊢ (((φ \land Y = \emptyset) \land t \in B) \land t = X) \to G (t) = G (X)$
38		simpllr	$⊢ (((φ \land Y = \emptyset) \land t \in B) \land t = X) \to Y = \emptyset$
39	35 37 38	3eqtr4rd	$⊢ (((φ \land Y = \emptyset) \land t \in B) \land t = X) \to Y = G (t)$
40		eqidd	$⊢ (((φ \land Y = \emptyset) \land t \in B) \land \neg t = X) \to G (t) = G (t)$
41	39 40	ifeqda	$⊢ ((φ \land Y = \emptyset) \land t \in B) \to if (t = X, Y, G (t)) = G (t)$
42	41	mpteq2dva	$⊢ (φ \land Y = \emptyset) \to (t \in B ⟼ if (t = X, Y, G (t))) = (t \in B ⟼ G (t))$
43	8 42	syl5eq	$⊢ (φ \land Y = \emptyset) \to F = (t \in B ⟼ G (t))$
44	19	feqmptd	$⊢ φ \to G = (t \in B ⟼ G (t))$
45	44	adantr	$⊢ (φ \land Y = \emptyset) \to G = (t \in B ⟼ G (t))$
46	43 45	eqtr4d	$⊢ (φ \land Y = \emptyset) \to F = G$
47	4	adantr	$⊢ (φ \land Y = \emptyset) \to G \in S$
48	46 47	eqeltrd	$⊢ (φ \land Y = \emptyset) \to F \in S$
49		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
50	2 3 49	syl2anc	$⊢ φ \to A ↑_{𝑜} B \in On$
51	1 2 3	cantnff	$⊢ φ \to (A CNF B) : S ⟶ A ↑_{𝑜} B$
52	51 4	ffvelrnd	$⊢ φ \to (A CNF B) (G) \in (A ↑_{𝑜} B)$
53		onelon	$⊢ (A ↑_{𝑜} B \in On \land (A CNF B) (G) \in (A ↑_{𝑜} B)) \to (A CNF B) (G) \in On$
54	50 52 53	syl2anc	$⊢ φ \to (A CNF B) (G) \in On$
55	54	adantr	$⊢ (φ \land Y = \emptyset) \to (A CNF B) (G) \in On$
56		oa0r	$⊢ (A CNF B) (G) \in On \to \emptyset +_{𝑜} (A CNF B) (G) = (A CNF B) (G)$
57	55 56	syl	$⊢ (φ \land Y = \emptyset) \to \emptyset +_{𝑜} (A CNF B) (G) = (A CNF B) (G)$
58		oveq2	$⊢ Y = \emptyset \to (A ↑_{𝑜} X) \cdot_{𝑜} Y = (A ↑_{𝑜} X) \cdot_{𝑜} \emptyset$
59		oecl	$⊢ (A \in On \land X \in On) \to A ↑_{𝑜} X \in On$
60	2 10 59	syl2anc	$⊢ φ \to A ↑_{𝑜} X \in On$
61		om0	$⊢ A ↑_{𝑜} X \in On \to (A ↑_{𝑜} X) \cdot_{𝑜} \emptyset = \emptyset$
62	60 61	syl	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} \emptyset = \emptyset$
63	58 62	sylan9eqr	$⊢ (φ \land Y = \emptyset) \to (A ↑_{𝑜} X) \cdot_{𝑜} Y = \emptyset$
64	63	oveq1d	$⊢ (φ \land Y = \emptyset) \to ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G) = \emptyset +_{𝑜} (A CNF B) (G)$
65	46	fveq2d	$⊢ (φ \land Y = \emptyset) \to (A CNF B) (F) = (A CNF B) (G)$
66	57 64 65	3eqtr4rd	$⊢ (φ \land Y = \emptyset) \to (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G)$
67	48 66	jca	$⊢ (φ \land Y = \emptyset) \to (F \in S \land (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G))$
68	2	adantr	$⊢ (φ \land Y \neq \emptyset) \to A \in On$
69	3	adantr	$⊢ (φ \land Y \neq \emptyset) \to B \in On$
70	4	adantr	$⊢ (φ \land Y \neq \emptyset) \to G \in S$
71	5	adantr	$⊢ (φ \land Y \neq \emptyset) \to X \in B$
72	6	adantr	$⊢ (φ \land Y \neq \emptyset) \to Y \in A$
73	7	adantr	$⊢ (φ \land Y \neq \emptyset) \to G supp \emptyset \subseteq X$
74	1 68 69 70 71 72 73 8	cantnfp1lem1	$⊢ (φ \land Y \neq \emptyset) \to F \in S$
75		onelon	$⊢ (A \in On \land Y \in A) \to Y \in On$
76	2 6 75	syl2anc	$⊢ φ \to Y \in On$
77		on0eln0	$⊢ Y \in On \to (\emptyset \in Y \leftrightarrow Y \neq \emptyset)$
78	76 77	syl	$⊢ φ \to (\emptyset \in Y \leftrightarrow Y \neq \emptyset)$
79	78	biimpar	$⊢ (φ \land Y \neq \emptyset) \to \emptyset \in Y$
80		eqid	$⊢ OrdIso (E, F supp \emptyset) = OrdIso (E, F supp \emptyset)$
81		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, F supp \emptyset) (k)) \cdot_{𝑜} F (OrdIso (E, F supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, F supp \emptyset) (k)) \cdot_{𝑜} F (OrdIso (E, F supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
82		eqid	$⊢ OrdIso (E, G supp \emptyset) = OrdIso (E, G supp \emptyset)$
83		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, G supp \emptyset) (k)) \cdot_{𝑜} G (OrdIso (E, G supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, G supp \emptyset) (k)) \cdot_{𝑜} G (OrdIso (E, G supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
84	1 68 69 70 71 72 73 8 79 80 81 82 83	cantnfp1lem3	$⊢ (φ \land Y \neq \emptyset) \to (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G)$
85	74 84	jca	$⊢ (φ \land Y \neq \emptyset) \to (F \in S \land (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G))$
86	67 85	pm2.61dane	$⊢ φ \to (F \in S \land (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G))$

Metamath Proof Explorer

Theorem cantnfp1

Proof