Theorem 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	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	cantnfp1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
	cantnfp1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cantnfp1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	cantnfp1.s	⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝑋 )
	cantnfp1.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) )
Assertion	cantnfp1	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		cantnfp1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
5		cantnfp1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		cantnfp1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
7		cantnfp1.s	⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝑋 )
8		cantnfp1.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) )
9		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ On )
10	3 5 9	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ On )
11		eloni	⊢ ( 𝑋 ∈ On → Ord 𝑋 )
12		ordirr	⊢ ( Ord 𝑋 → ¬ 𝑋 ∈ 𝑋 )
13	10 11 12	3syl	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑋 )
14		fvex	⊢ ( 𝐺 ‘ 𝑋 ) ∈ V
15		dif1o	⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ V ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) )
16	14 15	mpbiran	⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ↔ ( 𝐺 ‘ 𝑋 ) ≠ ∅ )
17	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
18	4 17	mpbid	⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
19	18	simpld	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
20	19	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
21		0ex	⊢ ∅ ∈ V
22	21	a1i	⊢ ( 𝜑 → ∅ ∈ V )
23		elsuppfn	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
24	20 3 22 23	syl3anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
25	16	bicomi	⊢ ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ ↔ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) )
26	25	a1i	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ ↔ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) )
27	26	anbi2d	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) ) )
28	24 27	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) ) )
29	7	sseld	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) → 𝑋 ∈ 𝑋 ) )
30	28 29	sylbird	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) → 𝑋 ∈ 𝑋 ) )
31	5 30	mpand	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) → 𝑋 ∈ 𝑋 ) )
32	16 31	biimtrrid	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ 𝑋 ) )
33	32	necon1bd	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ 𝑋 → ( 𝐺 ‘ 𝑋 ) = ∅ ) )
34	13 33	mpd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ∅ )
35	34	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑡 = 𝑋 ) → ( 𝐺 ‘ 𝑋 ) = ∅ )
36		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑡 = 𝑋 ) → 𝑡 = 𝑋 )
37	36	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑡 = 𝑋 ) → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑋 ) )
38		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑡 = 𝑋 ) → 𝑌 = ∅ )
39	35 37 38	3eqtr4rd	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑡 = 𝑋 ) → 𝑌 = ( 𝐺 ‘ 𝑡 ) )
40		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) ∧ ¬ 𝑡 = 𝑋 ) → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑡 ) )
41	39 40	ifeqda	⊢ ( ( ( 𝜑 ∧ 𝑌 = ∅ ) ∧ 𝑡 ∈ 𝐵 ) → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) = ( 𝐺 ‘ 𝑡 ) )
42	41	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑡 ) ) )
43	8 42	eqtrid	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → 𝐹 = ( 𝑡 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑡 ) ) )
44	19	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑡 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑡 ) ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → 𝐺 = ( 𝑡 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑡 ) ) )
46	43 45	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → 𝐹 = 𝐺 )
47	4	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → 𝐺 ∈ 𝑆 )
48	46 47	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → 𝐹 ∈ 𝑆 )
49		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
50	2 3 49	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On )
51	1 2 3	cantnff	⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) )
52	51 4	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ∈ ( 𝐴 ↑o 𝐵 ) )
53		onelon	⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ∈ On )
54	50 52 53	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ∈ On )
55	54	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ∈ On )
56		oa0r	⊢ ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ∈ On → ( ∅ +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )
57	55 56	syl	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( ∅ +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )
58		oveq2	⊢ ( 𝑌 = ∅ → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) = ( ( 𝐴 ↑o 𝑋 ) ·o ∅ ) )
59		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐴 ↑o 𝑋 ) ∈ On )
60	2 10 59	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ∈ On )
61		om0	⊢ ( ( 𝐴 ↑o 𝑋 ) ∈ On → ( ( 𝐴 ↑o 𝑋 ) ·o ∅ ) = ∅ )
62	60 61	syl	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o ∅ ) = ∅ )
63	58 62	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) = ∅ )
64	63	oveq1d	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) = ( ∅ +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )
65	46	fveq2d	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )
66	57 64 65	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )
67	48 66	jca	⊢ ( ( 𝜑 ∧ 𝑌 = ∅ ) → ( 𝐹 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) ) )
68	2	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → 𝐴 ∈ On )
69	3	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → 𝐵 ∈ On )
70	4	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → 𝐺 ∈ 𝑆 )
71	5	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → 𝑋 ∈ 𝐵 )
72	6	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → 𝑌 ∈ 𝐴 )
73	7	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → ( 𝐺 supp ∅ ) ⊆ 𝑋 )
74	1 68 69 70 71 72 73 8	cantnfp1lem1	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → 𝐹 ∈ 𝑆 )
75		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ On )
76	2 6 75	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ On )
77		on0eln0	⊢ ( 𝑌 ∈ On → ( ∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅ ) )
78	76 77	syl	⊢ ( 𝜑 → ( ∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅ ) )
79	78	biimpar	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → ∅ ∈ 𝑌 )
80		eqid	⊢ OrdIso ( E , ( 𝐹 supp ∅ ) ) = OrdIso ( E , ( 𝐹 supp ∅ ) )
81		eqid	⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
82		eqid	⊢ OrdIso ( E , ( 𝐺 supp ∅ ) ) = OrdIso ( E , ( 𝐺 supp ∅ ) )
83		eqid	⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐺 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐺 ‘ ( OrdIso ( E , ( 𝐺 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐺 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐺 ‘ ( OrdIso ( E , ( 𝐺 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
84	1 68 69 70 71 72 73 8 79 80 81 82 83	cantnfp1lem3	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )
85	74 84	jca	⊢ ( ( 𝜑 ∧ 𝑌 ≠ ∅ ) → ( 𝐹 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) ) )
86	67 85	pm2.61dane	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) ) )