| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑆 = dom ( ω CNF 𝑋 ) ) |
| 2 |
1
|
eleq2d |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ 𝑆 ↔ 𝑓 ∈ dom ( ω CNF 𝑋 ) ) ) |
| 3 |
|
eqid |
⊢ dom ( ω CNF 𝑋 ) = dom ( ω CNF 𝑋 ) |
| 4 |
|
omelon |
⊢ ω ∈ On |
| 5 |
4
|
a1i |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ω ∈ On ) |
| 6 |
|
simpl |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑋 ∈ On ) |
| 7 |
3 5 6
|
cantnfs |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ) |
| 8 |
2 7
|
bitrd |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ 𝑆 ↔ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ) |
| 9 |
1
|
eleq2d |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑔 ∈ 𝑆 ↔ 𝑔 ∈ dom ( ω CNF 𝑋 ) ) ) |
| 10 |
3 5 6
|
cantnfs |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑔 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ) |
| 11 |
9 10
|
bitrd |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑔 ∈ 𝑆 ↔ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ) |
| 12 |
11
|
adantr |
⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) → ( 𝑔 ∈ 𝑆 ↔ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ) |
| 13 |
|
simpl |
⊢ ( ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) → 𝑓 : 𝑋 ⟶ ω ) |
| 14 |
|
simpl |
⊢ ( ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) → 𝑔 : 𝑋 ⟶ ω ) |
| 15 |
13 14
|
anim12i |
⊢ ( ( ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) |
| 16 |
6 15
|
anim12i |
⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ) → ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ) |
| 17 |
16
|
anassrs |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ) |
| 18 |
|
simprl |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → 𝑓 : 𝑋 ⟶ ω ) |
| 19 |
18
|
ffnd |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → 𝑓 Fn 𝑋 ) |
| 20 |
|
simprr |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → 𝑔 : 𝑋 ⟶ ω ) |
| 21 |
20
|
ffnd |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → 𝑔 Fn 𝑋 ) |
| 22 |
|
simpl |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → 𝑋 ∈ On ) |
| 23 |
|
inidm |
⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋 |
| 24 |
19 21 22 22 23
|
offn |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ) |
| 25 |
|
simpr |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ) → ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ) |
| 26 |
|
simplrl |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑓 : 𝑋 ⟶ ω ) |
| 27 |
26
|
ffnd |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑓 Fn 𝑋 ) |
| 28 |
|
simplrr |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑔 : 𝑋 ⟶ ω ) |
| 29 |
28
|
ffnd |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑔 Fn 𝑋 ) |
| 30 |
|
simpll |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ On ) |
| 31 |
|
simpr |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 ) |
| 32 |
|
fnfvof |
⊢ ( ( ( 𝑓 Fn 𝑋 ∧ 𝑔 Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) +o ( 𝑔 ‘ 𝑥 ) ) ) |
| 33 |
27 29 30 31 32
|
syl22anc |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) +o ( 𝑔 ‘ 𝑥 ) ) ) |
| 34 |
18
|
ffvelcdmda |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑥 ) ∈ ω ) |
| 35 |
20
|
ffvelcdmda |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑥 ) ∈ ω ) |
| 36 |
|
nnacl |
⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ω ∧ ( 𝑔 ‘ 𝑥 ) ∈ ω ) → ( ( 𝑓 ‘ 𝑥 ) +o ( 𝑔 ‘ 𝑥 ) ) ∈ ω ) |
| 37 |
34 35 36
|
syl2anc |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ‘ 𝑥 ) +o ( 𝑔 ‘ 𝑥 ) ) ∈ ω ) |
| 38 |
33 37
|
eqeltrd |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) ∈ ω ) |
| 39 |
38
|
ex |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → ( 𝑥 ∈ 𝑋 → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) ∈ ω ) ) |
| 40 |
39
|
ralrimiv |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) ∈ ω ) |
| 41 |
40
|
adantr |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) ∈ ω ) |
| 42 |
|
fnfvrnss |
⊢ ( ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑥 ) ∈ ω ) → ran ( 𝑓 ∘f +o 𝑔 ) ⊆ ω ) |
| 43 |
25 41 42
|
syl2anc |
⊢ ( ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ) → ran ( 𝑓 ∘f +o 𝑔 ) ⊆ ω ) |
| 44 |
43
|
ex |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 → ran ( 𝑓 ∘f +o 𝑔 ) ⊆ ω ) ) |
| 45 |
24 44
|
jcai |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ∧ ran ( 𝑓 ∘f +o 𝑔 ) ⊆ ω ) ) |
| 46 |
|
df-f |
⊢ ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ↔ ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝑋 ∧ ran ( 𝑓 ∘f +o 𝑔 ) ⊆ ω ) ) |
| 47 |
45 46
|
sylibr |
⊢ ( ( 𝑋 ∈ On ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑔 : 𝑋 ⟶ ω ) ) → ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) |
| 48 |
17 47
|
syl |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) |
| 49 |
|
ffun |
⊢ ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω → Fun ( 𝑓 ∘f +o 𝑔 ) ) |
| 50 |
49
|
adantl |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → Fun ( 𝑓 ∘f +o 𝑔 ) ) |
| 51 |
|
simplrr |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → 𝑓 finSupp ∅ ) |
| 52 |
51
|
adantr |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → 𝑓 finSupp ∅ ) |
| 53 |
|
simplrr |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → 𝑔 finSupp ∅ ) |
| 54 |
52 53
|
fsuppunfi |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( ( 𝑓 supp ∅ ) ∪ ( 𝑔 supp ∅ ) ) ∈ Fin ) |
| 55 |
|
simp-4l |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → 𝑋 ∈ On ) |
| 56 |
|
peano1 |
⊢ ∅ ∈ ω |
| 57 |
56
|
a1i |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ∅ ∈ ω ) |
| 58 |
|
simplrl |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → 𝑓 : 𝑋 ⟶ ω ) |
| 59 |
58
|
adantr |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → 𝑓 : 𝑋 ⟶ ω ) |
| 60 |
|
simplrl |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → 𝑔 : 𝑋 ⟶ ω ) |
| 61 |
|
0elon |
⊢ ∅ ∈ On |
| 62 |
|
oa0 |
⊢ ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ ) |
| 63 |
61 62
|
mp1i |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( ∅ +o ∅ ) = ∅ ) |
| 64 |
55 57 59 60 63
|
suppofssd |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( ( 𝑓 ∘f +o 𝑔 ) supp ∅ ) ⊆ ( ( 𝑓 supp ∅ ) ∪ ( 𝑔 supp ∅ ) ) ) |
| 65 |
54 64
|
ssfid |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( ( 𝑓 ∘f +o 𝑔 ) supp ∅ ) ∈ Fin ) |
| 66 |
|
ovexd |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( 𝑓 ∘f +o 𝑔 ) ∈ V ) |
| 67 |
|
isfsupp |
⊢ ( ( ( 𝑓 ∘f +o 𝑔 ) ∈ V ∧ ∅ ∈ On ) → ( ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ↔ ( Fun ( 𝑓 ∘f +o 𝑔 ) ∧ ( ( 𝑓 ∘f +o 𝑔 ) supp ∅ ) ∈ Fin ) ) ) |
| 68 |
66 61 67
|
sylancl |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ↔ ( Fun ( 𝑓 ∘f +o 𝑔 ) ∧ ( ( 𝑓 ∘f +o 𝑔 ) supp ∅ ) ∈ Fin ) ) ) |
| 69 |
50 65 68
|
mpbir2and |
⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) ∧ ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ) → ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ) |
| 70 |
69
|
ex |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω → ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ) ) |
| 71 |
48 70
|
jcai |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ∧ ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ) ) |
| 72 |
1
|
eleq2d |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ↔ ( 𝑓 ∘f +o 𝑔 ) ∈ dom ( ω CNF 𝑋 ) ) ) |
| 73 |
3 5 6
|
cantnfs |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ∈ dom ( ω CNF 𝑋 ) ↔ ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ∧ ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ) ) ) |
| 74 |
72 73
|
bitrd |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ↔ ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ∧ ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ) ) ) |
| 75 |
74
|
ad2antrr |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ↔ ( ( 𝑓 ∘f +o 𝑔 ) : 𝑋 ⟶ ω ∧ ( 𝑓 ∘f +o 𝑔 ) finSupp ∅ ) ) ) |
| 76 |
71 75
|
mpbird |
⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) ∧ ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) ) → ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) |
| 77 |
76
|
ex |
⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) → ( ( 𝑔 : 𝑋 ⟶ ω ∧ 𝑔 finSupp ∅ ) → ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) ) |
| 78 |
12 77
|
sylbid |
⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) → ( 𝑔 ∈ 𝑆 → ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) ) |
| 79 |
78
|
ralrimiv |
⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) → ∀ 𝑔 ∈ 𝑆 ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) |
| 80 |
79
|
ex |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) → ∀ 𝑔 ∈ 𝑆 ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) ) |
| 81 |
8 80
|
sylbid |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ 𝑆 → ∀ 𝑔 ∈ 𝑆 ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) ) |
| 82 |
81
|
ralrimiv |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ∀ 𝑓 ∈ 𝑆 ∀ 𝑔 ∈ 𝑆 ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ) |
| 83 |
|
ofmres |
⊢ ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) = ( 𝑓 ∈ 𝑆 , 𝑔 ∈ 𝑆 ↦ ( 𝑓 ∘f +o 𝑔 ) ) |
| 84 |
83
|
fmpo |
⊢ ( ∀ 𝑓 ∈ 𝑆 ∀ 𝑔 ∈ 𝑆 ( 𝑓 ∘f +o 𝑔 ) ∈ 𝑆 ↔ ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) ⟶ 𝑆 ) |
| 85 |
82 84
|
sylib |
⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) ⟶ 𝑆 ) |