Metamath Proof Explorer

Theorem ofoafg

Description: Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoafg ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ( ∘f +o ↾ ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) : ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ⟶ ( 𝐹 ↑m 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) → 𝐷 ∈ On )
2 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → 𝐴 ∈ 𝑉 )
3 elmapg ⊢ ( ( 𝐷 ∈ On ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐷 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐷 ) )
4 1 2 3 syl2anr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ( 𝑓 ∈ ( 𝐷 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐷 ) )
5 simp2 ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) → 𝐸 ∈ On )
6 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ∈ 𝑊 )
7 elmapg ⊢ ( ( 𝐸 ∈ On ∧ 𝐵 ∈ 𝑊 ) → ( 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ↔ 𝑔 : 𝐵 ⟶ 𝐸 ) )
8 5 6 7 syl2anr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ( 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ↔ 𝑔 : 𝐵 ⟶ 𝐸 ) )
9 8 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ 𝑓 : 𝐴 ⟶ 𝐷 ) → ( 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ↔ 𝑔 : 𝐵 ⟶ 𝐸 ) )
10 simpl ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) → 𝑓 : 𝐴 ⟶ 𝐷 )
11 10 ffnd ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) → 𝑓 Fn 𝐴 )
12 11 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝑓 Fn 𝐴 )
13 simpr ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) → 𝑔 : 𝐵 ⟶ 𝐸 )
14 13 ffnd ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) → 𝑔 Fn 𝐵 )
15 14 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝑔 Fn 𝐵 )
16 2 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝐴 ∈ 𝑉 )
17 6 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝐵 ∈ 𝑊 )
18 eqid ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 )
19 12 15 16 17 18 offn ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ∘f +o 𝑔 ) Fn ( 𝐴 ∩ 𝐵 ) )
20 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → 𝐶 = ( 𝐴 ∩ 𝐵 ) )
21 20 fneq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ↔ ( 𝑓 ∘f +o 𝑔 ) Fn ( 𝐴 ∩ 𝐵 ) ) )
22 21 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ↔ ( 𝑓 ∘f +o 𝑔 ) Fn ( 𝐴 ∩ 𝐵 ) ) )
23 19 22 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 )
24 fresin ⊢ ( 𝑓 : 𝐴 ⟶ 𝐷 → ( 𝑓 ↾ 𝐶 ) : ( 𝐴 ∩ 𝐶 ) ⟶ 𝐷 )
25 24 adantr ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) → ( 𝑓 ↾ 𝐶 ) : ( 𝐴 ∩ 𝐶 ) ⟶ 𝐷 )
26 25 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ↾ 𝐶 ) : ( 𝐴 ∩ 𝐶 ) ⟶ 𝐷 )
27 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
28 20 27 eqsstrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ⊆ 𝐴 )
29 sseqin2 ⊢ ( 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐶 )
30 28 29 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐶 ) = 𝐶 )
31 30 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝐴 ∩ 𝐶 ) = 𝐶 )
32 31 feq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ↾ 𝐶 ) : ( 𝐴 ∩ 𝐶 ) ⟶ 𝐷 ↔ ( 𝑓 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 ) )
33 26 32 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 )
34 33 ffvelcdmda ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ 𝐷 )
35 5 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝐸 ∈ On )
36 1 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝐷 ∈ On )
37 onelon ⊢ ( ( 𝐷 ∈ On ∧ ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ 𝐷 ) → ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ On )
38 36 34 37 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ On )
39 fresin ⊢ ( 𝑔 : 𝐵 ⟶ 𝐸 → ( 𝑔 ↾ 𝐶 ) : ( 𝐵 ∩ 𝐶 ) ⟶ 𝐸 )
40 39 adantl ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) → ( 𝑔 ↾ 𝐶 ) : ( 𝐵 ∩ 𝐶 ) ⟶ 𝐸 )
41 40 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑔 ↾ 𝐶 ) : ( 𝐵 ∩ 𝐶 ) ⟶ 𝐸 )
42 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
43 20 42 eqsstrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ⊆ 𝐵 )
44 sseqin2 ⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐶 ) = 𝐶 )
45 43 44 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( 𝐵 ∩ 𝐶 ) = 𝐶 )
46 45 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝐵 ∩ 𝐶 ) = 𝐶 )
47 46 feq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑔 ↾ 𝐶 ) : ( 𝐵 ∩ 𝐶 ) ⟶ 𝐸 ↔ ( 𝑔 ↾ 𝐶 ) : 𝐶 ⟶ 𝐸 ) )
48 41 47 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑔 ↾ 𝐶 ) : 𝐶 ⟶ 𝐸 )
49 48 ffvelcdmda ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ∈ 𝐸 )
50 oaordi ⊢ ( ( 𝐸 ∈ On ∧ ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ On ) → ( ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ∈ 𝐸 → ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) ∈ ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o 𝐸 ) ) )
51 50 imp ⊢ ( ( ( 𝐸 ∈ On ∧ ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ On ) ∧ ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ∈ 𝐸 ) → ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) ∈ ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o 𝐸 ) )
52 35 38 49 51 syl21anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) ∈ ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o 𝐸 ) )
53 oveq1 ⊢ ( 𝑑 = ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) → ( 𝑑 +o 𝐸 ) = ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o 𝐸 ) )
54 53 eliuni ⊢ ( ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) ∈ 𝐷 ∧ ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) ∈ ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o 𝐸 ) ) → ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) ∈ ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) )
55 34 52 54 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) ∈ ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) )
56 12 15 16 17 18 ofres ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ∘f +o 𝑔 ) = ( ( 𝑓 ↾ ( 𝐴 ∩ 𝐵 ) ) ∘f +o ( 𝑔 ↾ ( 𝐴 ∩ 𝐵 ) ) ) )
57 20 reseq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( 𝑓 ↾ 𝐶 ) = ( 𝑓 ↾ ( 𝐴 ∩ 𝐵 ) ) )
58 20 reseq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( 𝑔 ↾ 𝐶 ) = ( 𝑔 ↾ ( 𝐴 ∩ 𝐵 ) ) )
59 57 58 oveq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) = ( ( 𝑓 ↾ ( 𝐴 ∩ 𝐵 ) ) ∘f +o ( 𝑔 ↾ ( 𝐴 ∩ 𝐵 ) ) ) )
60 59 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) = ( ( 𝑓 ↾ ( 𝐴 ∩ 𝐵 ) ) ∘f +o ( 𝑔 ↾ ( 𝐴 ∩ 𝐵 ) ) ) )
61 56 60 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ∘f +o 𝑔 ) = ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) )
62 61 fveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑐 ) = ( ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) ‘ 𝑐 ) )
63 62 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑐 ) = ( ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) ‘ 𝑐 ) )
64 28 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝐶 ⊆ 𝐴 )
65 12 64 fnssresd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ↾ 𝐶 ) Fn 𝐶 )
66 43 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝐶 ⊆ 𝐵 )
67 15 66 fnssresd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑔 ↾ 𝐶 ) Fn 𝐶 )
68 65 67 jca ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ↾ 𝐶 ) Fn 𝐶 ∧ ( 𝑔 ↾ 𝐶 ) Fn 𝐶 ) )
69 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )
70 2 69 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ V )
71 20 70 eqeltrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ∈ V )
72 71 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝐶 ∈ V )
73 72 anim1i ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝐶 ∈ V ∧ 𝑐 ∈ 𝐶 ) )
74 fnfvof ⊢ ( ( ( ( 𝑓 ↾ 𝐶 ) Fn 𝐶 ∧ ( 𝑔 ↾ 𝐶 ) Fn 𝐶 ) ∧ ( 𝐶 ∈ V ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) ‘ 𝑐 ) = ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) )
75 68 73 74 syl2an2r ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝑓 ↾ 𝐶 ) ∘f +o ( 𝑔 ↾ 𝐶 ) ) ‘ 𝑐 ) = ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) )
76 63 75 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑐 ) = ( ( ( 𝑓 ↾ 𝐶 ) ‘ 𝑐 ) +o ( ( 𝑔 ↾ 𝐶 ) ‘ 𝑐 ) ) )
77 simp3 ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) → 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) )
78 77 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) )
79 55 76 78 3eltr4d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑐 ) ∈ 𝐹 )
80 79 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ∀ 𝑐 ∈ 𝐶 ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑐 ) ∈ 𝐹 )
81 fnfvrnss ⊢ ( ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ∧ ∀ 𝑐 ∈ 𝐶 ( ( 𝑓 ∘f +o 𝑔 ) ‘ 𝑐 ) ∈ 𝐹 ) → ran ( 𝑓 ∘f +o 𝑔 ) ⊆ 𝐹 )
82 80 81 sylan2 ⊢ ( ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ∧ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) ) → ran ( 𝑓 ∘f +o 𝑔 ) ⊆ 𝐹 )
83 82 expcom ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 → ran ( 𝑓 ∘f +o 𝑔 ) ⊆ 𝐹 ) )
84 23 83 jcai ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ∧ ran ( 𝑓 ∘f +o 𝑔 ) ⊆ 𝐹 ) )
85 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ On )
86 85 adantlr ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ) ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ On )
87 simpr ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ) → 𝐸 ∈ On )
88 87 adantr ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ) ∧ 𝑑 ∈ 𝐷 ) → 𝐸 ∈ On )
89 oacl ⊢ ( ( 𝑑 ∈ On ∧ 𝐸 ∈ On ) → ( 𝑑 +o 𝐸 ) ∈ On )
90 86 88 89 syl2anc ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝑑 +o 𝐸 ) ∈ On )
91 90 ralrimiva ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ) → ∀ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ∈ On )
92 iunon ⊢ ( ( 𝐷 ∈ On ∧ ∀ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ∈ On ) → ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ∈ On )
93 91 92 syldan ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ) → ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ∈ On )
94 93 3adant3 ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) → ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ∈ On )
95 77 94 eqeltrd ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) → 𝐹 ∈ On )
96 95 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → 𝐹 ∈ On )
97 96 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → 𝐹 ∈ On )
98 97 72 elmapd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ↔ ( 𝑓 ∘f +o 𝑔 ) : 𝐶 ⟶ 𝐹 ) )
99 df-f ⊢ ( ( 𝑓 ∘f +o 𝑔 ) : 𝐶 ⟶ 𝐹 ↔ ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ∧ ran ( 𝑓 ∘f +o 𝑔 ) ⊆ 𝐹 ) )
100 98 99 bitrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ↔ ( ( 𝑓 ∘f +o 𝑔 ) Fn 𝐶 ∧ ran ( 𝑓 ∘f +o 𝑔 ) ⊆ 𝐹 ) ) )
101 84 100 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐷 ∧ 𝑔 : 𝐵 ⟶ 𝐸 ) ) → ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) )
102 101 expr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ 𝑓 : 𝐴 ⟶ 𝐷 ) → ( 𝑔 : 𝐵 ⟶ 𝐸 → ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ) )
103 9 102 sylbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ 𝑓 : 𝐴 ⟶ 𝐷 ) → ( 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) → ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ) )
104 103 ralrimiv ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) ∧ 𝑓 : 𝐴 ⟶ 𝐷 ) → ∀ 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) )
105 104 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ( 𝑓 : 𝐴 ⟶ 𝐷 → ∀ 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ) )
106 4 105 sylbid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ( 𝑓 ∈ ( 𝐷 ↑m 𝐴 ) → ∀ 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ) )
107 106 ralrimiv ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ∀ 𝑓 ∈ ( 𝐷 ↑m 𝐴 ) ∀ 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) )
108 ofmres ⊢ ( ∘f +o ↾ ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) = ( 𝑓 ∈ ( 𝐷 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ↦ ( 𝑓 ∘f +o 𝑔 ) )
109 108 fmpo ⊢ ( ∀ 𝑓 ∈ ( 𝐷 ↑m 𝐴 ) ∀ 𝑔 ∈ ( 𝐸 ↑m 𝐵 ) ( 𝑓 ∘f +o 𝑔 ) ∈ ( 𝐹 ↑m 𝐶 ) ↔ ( ∘f +o ↾ ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) : ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ⟶ ( 𝐹 ↑m 𝐶 ) )
110 107 109 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 ( 𝑑 +o 𝐸 ) ) ) → ( ∘f +o ↾ ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) : ( ( 𝐷 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ⟶ ( 𝐹 ↑m 𝐶 ) )