Metamath Proof Explorer

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 𝐵 ) ‘ 𝐺 ) ) ) )