| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . 6
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → 𝑆 = dom (ω CNF 𝑋)) | 
| 2 | 1 | eleq2d 2827 | . . . . 5
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑓 ∈ 𝑆 ↔ 𝑓 ∈ dom (ω CNF 𝑋))) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢ dom
(ω CNF 𝑋) = dom
(ω CNF 𝑋) | 
| 4 |  | omelon 9686 | . . . . . . 7
⊢ ω
∈ On | 
| 5 | 4 | a1i 11 | . . . . . 6
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ω ∈
On) | 
| 6 |  | simpl 482 | . . . . . 6
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → 𝑋 ∈ On) | 
| 7 | 3, 5, 6 | cantnfs 9706 | . . . . 5
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑓 ∈ dom (ω CNF 𝑋) ↔ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅))) | 
| 8 | 2, 7 | bitrd 279 | . . . 4
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑓 ∈ 𝑆 ↔ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅))) | 
| 9 | 1 | eleq2d 2827 | . . . . . . . . 9
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑔 ∈ 𝑆 ↔ 𝑔 ∈ dom (ω CNF 𝑋))) | 
| 10 | 3, 5, 6 | cantnfs 9706 | . . . . . . . . 9
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑔 ∈ dom (ω CNF 𝑋) ↔ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅))) | 
| 11 | 9, 10 | bitrd 279 | . . . . . . . 8
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑔 ∈ 𝑆 ↔ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅))) | 
| 12 | 11 | adantr 480 | . . . . . . 7
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) → (𝑔 ∈ 𝑆 ↔ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅))) | 
| 13 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅) → 𝑓:𝑋⟶ω) | 
| 14 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅) → 𝑔:𝑋⟶ω) | 
| 15 | 13, 14 | anim12i 613 | . . . . . . . . . . . . 13
⊢ (((𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) | 
| 16 | 6, 15 | anim12i 613 | . . . . . . . . . . . 12
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ ((𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅))) → (𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω))) | 
| 17 | 16 | anassrs 467 | . . . . . . . . . . 11
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → (𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω))) | 
| 18 |  | simprl 771 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → 𝑓:𝑋⟶ω) | 
| 19 | 18 | ffnd 6737 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → 𝑓 Fn 𝑋) | 
| 20 |  | simprr 773 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → 𝑔:𝑋⟶ω) | 
| 21 | 20 | ffnd 6737 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → 𝑔 Fn 𝑋) | 
| 22 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → 𝑋 ∈ On) | 
| 23 |  | inidm 4227 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∩ 𝑋) = 𝑋 | 
| 24 | 19, 21, 22, 22, 23 | offn 7710 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → (𝑓 ∘f +o 𝑔) Fn 𝑋) | 
| 25 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ (𝑓 ∘f +o 𝑔) Fn 𝑋) → (𝑓 ∘f +o 𝑔) Fn 𝑋) | 
| 26 |  | simplrl 777 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → 𝑓:𝑋⟶ω) | 
| 27 | 26 | ffnd 6737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → 𝑓 Fn 𝑋) | 
| 28 |  | simplrr 778 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → 𝑔:𝑋⟶ω) | 
| 29 | 28 | ffnd 6737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → 𝑔 Fn 𝑋) | 
| 30 |  | simpll 767 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ On) | 
| 31 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 32 |  | fnfvof 7714 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 Fn 𝑋 ∧ 𝑔 Fn 𝑋) ∧ (𝑋 ∈ On ∧ 𝑥 ∈ 𝑋)) → ((𝑓 ∘f +o 𝑔)‘𝑥) = ((𝑓‘𝑥) +o (𝑔‘𝑥))) | 
| 33 | 27, 29, 30, 31, 32 | syl22anc 839 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → ((𝑓 ∘f +o 𝑔)‘𝑥) = ((𝑓‘𝑥) +o (𝑔‘𝑥))) | 
| 34 | 18 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → (𝑓‘𝑥) ∈ ω) | 
| 35 | 20 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ ω) | 
| 36 |  | nnacl 8649 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓‘𝑥) ∈ ω ∧ (𝑔‘𝑥) ∈ ω) → ((𝑓‘𝑥) +o (𝑔‘𝑥)) ∈ ω) | 
| 37 | 34, 35, 36 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → ((𝑓‘𝑥) +o (𝑔‘𝑥)) ∈ ω) | 
| 38 | 33, 37 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ 𝑥 ∈ 𝑋) → ((𝑓 ∘f +o 𝑔)‘𝑥) ∈ ω) | 
| 39 | 38 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → (𝑥 ∈ 𝑋 → ((𝑓 ∘f +o 𝑔)‘𝑥) ∈ ω)) | 
| 40 | 39 | ralrimiv 3145 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → ∀𝑥 ∈ 𝑋 ((𝑓 ∘f +o 𝑔)‘𝑥) ∈ ω) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ (𝑓 ∘f +o 𝑔) Fn 𝑋) → ∀𝑥 ∈ 𝑋 ((𝑓 ∘f +o 𝑔)‘𝑥) ∈ ω) | 
| 42 |  | fnfvrnss 7141 | . . . . . . . . . . . . . . 15
⊢ (((𝑓 ∘f
+o 𝑔) Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 ((𝑓 ∘f +o 𝑔)‘𝑥) ∈ ω) → ran (𝑓 ∘f
+o 𝑔) ⊆
ω) | 
| 43 | 25, 41, 42 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) ∧ (𝑓 ∘f +o 𝑔) Fn 𝑋) → ran (𝑓 ∘f +o 𝑔) ⊆
ω) | 
| 44 | 43 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → ((𝑓 ∘f
+o 𝑔) Fn 𝑋 → ran (𝑓 ∘f +o 𝑔) ⊆
ω)) | 
| 45 | 24, 44 | jcai 516 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → ((𝑓 ∘f
+o 𝑔) Fn 𝑋 ∧ ran (𝑓 ∘f +o 𝑔) ⊆
ω)) | 
| 46 |  | df-f 6565 | . . . . . . . . . . . 12
⊢ ((𝑓 ∘f
+o 𝑔):𝑋⟶ω ↔ ((𝑓 ∘f
+o 𝑔) Fn 𝑋 ∧ ran (𝑓 ∘f +o 𝑔) ⊆
ω)) | 
| 47 | 45, 46 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ On ∧ (𝑓:𝑋⟶ω ∧ 𝑔:𝑋⟶ω)) → (𝑓 ∘f +o 𝑔):𝑋⟶ω) | 
| 48 | 17, 47 | syl 17 | . . . . . . . . . 10
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → (𝑓 ∘f +o 𝑔):𝑋⟶ω) | 
| 49 |  | ffun 6739 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∘f
+o 𝑔):𝑋⟶ω → Fun
(𝑓 ∘f
+o 𝑔)) | 
| 50 | 49 | adantl 481 | . . . . . . . . . . . 12
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → Fun (𝑓 ∘f
+o 𝑔)) | 
| 51 |  | simplrr 778 | . . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → 𝑓 finSupp ∅) | 
| 52 | 51 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → 𝑓 finSupp ∅) | 
| 53 |  | simplrr 778 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → 𝑔 finSupp ∅) | 
| 54 | 52, 53 | fsuppunfi 9428 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → ((𝑓 supp ∅) ∪ (𝑔 supp ∅)) ∈ Fin) | 
| 55 |  | simp-4l 783 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → 𝑋 ∈ On) | 
| 56 |  | peano1 7910 | . . . . . . . . . . . . . . 15
⊢ ∅
∈ ω | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → ∅ ∈
ω) | 
| 58 |  | simplrl 777 | . . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → 𝑓:𝑋⟶ω) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → 𝑓:𝑋⟶ω) | 
| 60 |  | simplrl 777 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → 𝑔:𝑋⟶ω) | 
| 61 |  | 0elon 6438 | . . . . . . . . . . . . . . 15
⊢ ∅
∈ On | 
| 62 |  | oa0 8554 | . . . . . . . . . . . . . . 15
⊢ (∅
∈ On → (∅ +o ∅) = ∅) | 
| 63 | 61, 62 | mp1i 13 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → (∅
+o ∅) = ∅) | 
| 64 | 55, 57, 59, 60, 63 | suppofssd 8228 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → ((𝑓 ∘f +o 𝑔) supp ∅) ⊆ ((𝑓 supp ∅) ∪ (𝑔 supp
∅))) | 
| 65 | 54, 64 | ssfid 9301 | . . . . . . . . . . . 12
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → ((𝑓 ∘f +o 𝑔) supp ∅) ∈
Fin) | 
| 66 |  | ovexd 7466 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → (𝑓 ∘f +o 𝑔) ∈ V) | 
| 67 |  | isfsupp 9405 | . . . . . . . . . . . . 13
⊢ (((𝑓 ∘f
+o 𝑔) ∈ V
∧ ∅ ∈ On) → ((𝑓 ∘f +o 𝑔) finSupp ∅ ↔ (Fun
(𝑓 ∘f
+o 𝑔) ∧
((𝑓 ∘f
+o 𝑔) supp
∅) ∈ Fin))) | 
| 68 | 66, 61, 67 | sylancl 586 | . . . . . . . . . . . 12
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → ((𝑓 ∘f +o 𝑔) finSupp ∅ ↔ (Fun
(𝑓 ∘f
+o 𝑔) ∧
((𝑓 ∘f
+o 𝑔) supp
∅) ∈ Fin))) | 
| 69 | 50, 65, 68 | mpbir2and 713 | . . . . . . . . . . 11
⊢
(((((𝑋 ∈ On
∧ 𝑆 = dom (ω CNF
𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) ∧ (𝑓 ∘f +o 𝑔):𝑋⟶ω) → (𝑓 ∘f +o 𝑔) finSupp
∅) | 
| 70 | 69 | ex 412 | . . . . . . . . . 10
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → ((𝑓 ∘f
+o 𝑔):𝑋⟶ω → (𝑓 ∘f
+o 𝑔) finSupp
∅)) | 
| 71 | 48, 70 | jcai 516 | . . . . . . . . 9
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → ((𝑓 ∘f
+o 𝑔):𝑋⟶ω ∧ (𝑓 ∘f
+o 𝑔) finSupp
∅)) | 
| 72 | 1 | eleq2d 2827 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ((𝑓 ∘f +o 𝑔) ∈ 𝑆 ↔ (𝑓 ∘f +o 𝑔) ∈ dom (ω CNF 𝑋))) | 
| 73 | 3, 5, 6 | cantnfs 9706 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ((𝑓 ∘f +o 𝑔) ∈ dom (ω CNF 𝑋) ↔ ((𝑓 ∘f +o 𝑔):𝑋⟶ω ∧ (𝑓 ∘f +o 𝑔) finSupp
∅))) | 
| 74 | 72, 73 | bitrd 279 | . . . . . . . . . 10
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ((𝑓 ∘f +o 𝑔) ∈ 𝑆 ↔ ((𝑓 ∘f +o 𝑔):𝑋⟶ω ∧ (𝑓 ∘f +o 𝑔) finSupp
∅))) | 
| 75 | 74 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → ((𝑓 ∘f
+o 𝑔) ∈
𝑆 ↔ ((𝑓 ∘f
+o 𝑔):𝑋⟶ω ∧ (𝑓 ∘f
+o 𝑔) finSupp
∅))) | 
| 76 | 71, 75 | mpbird 257 | . . . . . . . 8
⊢ ((((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) ∧ (𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅)) → (𝑓 ∘f +o 𝑔) ∈ 𝑆) | 
| 77 | 76 | ex 412 | . . . . . . 7
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) → ((𝑔:𝑋⟶ω ∧ 𝑔 finSupp ∅) → (𝑓 ∘f +o 𝑔) ∈ 𝑆)) | 
| 78 | 12, 77 | sylbid 240 | . . . . . 6
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) → (𝑔 ∈ 𝑆 → (𝑓 ∘f +o 𝑔) ∈ 𝑆)) | 
| 79 | 78 | ralrimiv 3145 | . . . . 5
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅)) → ∀𝑔 ∈ 𝑆 (𝑓 ∘f +o 𝑔) ∈ 𝑆) | 
| 80 | 79 | ex 412 | . . . 4
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ((𝑓:𝑋⟶ω ∧ 𝑓 finSupp ∅) → ∀𝑔 ∈ 𝑆 (𝑓 ∘f +o 𝑔) ∈ 𝑆)) | 
| 81 | 8, 80 | sylbid 240 | . . 3
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → (𝑓 ∈ 𝑆 → ∀𝑔 ∈ 𝑆 (𝑓 ∘f +o 𝑔) ∈ 𝑆)) | 
| 82 | 81 | ralrimiv 3145 | . 2
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ∀𝑓 ∈ 𝑆 ∀𝑔 ∈ 𝑆 (𝑓 ∘f +o 𝑔) ∈ 𝑆) | 
| 83 |  | ofmres 8009 | . . 3
⊢ (
∘f +o ↾ (𝑆 × 𝑆)) = (𝑓 ∈ 𝑆, 𝑔 ∈ 𝑆 ↦ (𝑓 ∘f +o 𝑔)) | 
| 84 | 83 | fmpo 8093 | . 2
⊢
(∀𝑓 ∈
𝑆 ∀𝑔 ∈ 𝑆 (𝑓 ∘f +o 𝑔) ∈ 𝑆 ↔ ( ∘f +o
↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)⟶𝑆) | 
| 85 | 82, 84 | sylib 218 | 1
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f
+o ↾ (𝑆
× 𝑆)):(𝑆 × 𝑆)⟶𝑆) |